Theorem dfss2OLD

Description: Obsolete version of dfss2 as of 16-May-2024. (Contributed by NM, 8-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dfss2OLD	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		dfss	|- ( A C_ B <-> A = ( A i^i B ) )
2		df-in	|- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
3	2	eqeq2i	|- ( A = ( A i^i B ) <-> A = { x | ( x e. A /\ x e. B ) } )
4		abeq2	|- ( A = { x | ( x e. A /\ x e. B ) } <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
5	1 3 4	3bitri	|- ( A C_ B <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
6		pm4.71	|- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
7	6	albii	|- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> ( x e. A /\ x e. B ) ) )
8	5 7	bitr4i	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )