Theorem dfss2

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. (Contributed by NM, 8-Jan-2002) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 16-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dfcleq	|- ( A = ( A i^i B ) <-> A. x ( x e. A <-> x e. ( A i^i B ) ) )
2		dfss	|- ( A C_ B <-> A = ( A i^i B ) )
3		pm4.71	|- ( ( x e. A -> x e. B ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
4		elin	|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
5	4	bibi2i	|- ( ( x e. A <-> x e. ( A i^i B ) ) <-> ( x e. A <-> ( x e. A /\ x e. B ) ) )
6	3 5	bitr4i	|- ( ( x e. A -> x e. B ) <-> ( x e. A <-> x e. ( A i^i B ) ) )
7	6	albii	|- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. A <-> x e. ( A i^i B ) ) )
8	1 2 7	3bitr4i	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )