Theorem inex1

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of TakeutiZaring p. 22. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	inex1.1	|- A e. _V
Assertion	inex1	|- ( A i^i B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		inex1.1	|- A e. _V
2	1	zfauscl	|- E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) )
3		dfcleq	|- ( x = ( A i^i B ) <-> A. y ( y e. x <-> y e. ( A i^i B ) ) )
4		elin	|- ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
5	4	bibi2i	|- ( ( y e. x <-> y e. ( A i^i B ) ) <-> ( y e. x <-> ( y e. A /\ y e. B ) ) )
6	5	albii	|- ( A. y ( y e. x <-> y e. ( A i^i B ) ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
7	3 6	bitri	|- ( x = ( A i^i B ) <-> A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
8	7	exbii	|- ( E. x x = ( A i^i B ) <-> E. x A. y ( y e. x <-> ( y e. A /\ y e. B ) ) )
9	2 8	mpbir	|- E. x x = ( A i^i B )
10	9	issetri	|- ( A i^i B ) e. _V