Theorem ssext

Description: An extensionality-like principle that uses the subset instead of the membership relation: two classes are equal iff they have the same subsets. (Contributed by NM, 30-Jun-2004)

	Ref	Expression
Assertion	ssext	|- ( A = B <-> A. x ( x C_ A <-> x C_ B ) )

Proof

Step	Hyp	Ref	Expression
1		ssextss	|- ( A C_ B <-> A. x ( x C_ A -> x C_ B ) )
2		ssextss	|- ( B C_ A <-> A. x ( x C_ B -> x C_ A ) )
3	1 2	anbi12i	|- ( ( A C_ B /\ B C_ A ) <-> ( A. x ( x C_ A -> x C_ B ) /\ A. x ( x C_ B -> x C_ A ) ) )
4		eqss	|- ( A = B <-> ( A C_ B /\ B C_ A ) )
5		albiim	|- ( A. x ( x C_ A <-> x C_ B ) <-> ( A. x ( x C_ A -> x C_ B ) /\ A. x ( x C_ B -> x C_ A ) ) )
6	3 4 5	3bitr4i	|- ( A = B <-> A. x ( x C_ A <-> x C_ B ) )