Proof of proveit.logic.sets.inclusion.subset_eq_via_equality theorem

see dependencies

import proveit
from proveit import defaults
from proveit import x, y, A, B, C, Px
from proveit.logic import And, Equals, Forall, Implies, SubsetEq
from proveit.logic.equality import sub_right_side_into
from proveit.logic.sets.inclusion  import subset_eq_def
from proveit.logic.sets.inclusion import subset_eq_reflexive
%proving subset_eq_via_equality

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
subset_eq_via_equality:
(see dependencies)

subset_eq_via_equality may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

subset_eq_reflexive

 ⊢  

subset_eq_reflexive_spec = subset_eq_reflexive.instantiate()

subset_eq_reflexive_spec:  ⊢  

sub_right_side_into

 ⊢  

sub_right_side_into.instantiate({Px:SubsetEq(A, x), x:A, y:B}, assumptions=[Equals(A, B)])

 ⊢  

%qed

proveit.logic.sets.inclusion.subset_eq_via_equality has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , : , :
2	theorem		⊢
	proveit.logic.equality.sub_right_side_into
3	instantiation	5	⊢
	:
4	assumption		⊢
5	theorem		⊢
	proveit.logic.sets.inclusion.subset_eq_reflexive