Theorem zfregs2VD

Description: Virtual deduction proof of zfregs2 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	zfregs2VD	|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )

Proof

Step	Hyp	Ref	Expression
1		idn1	|- (. A =/= (/) ->. A =/= (/) ).
2		zfregs	|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )
3	1 2	e1a	|- (. A =/= (/) ->. E. x e. A ( x i^i A ) = (/) ).
4		incom	|- ( x i^i A ) = ( A i^i x )
5	4	eqeq1i	|- ( ( x i^i A ) = (/) <-> ( A i^i x ) = (/) )
6	5	rexbii	|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A ( A i^i x ) = (/) )
7	3 6	e1bi	|- (. A =/= (/) ->. E. x e. A ( A i^i x ) = (/) ).
8		disj1	|- ( ( A i^i x ) = (/) <-> A. y ( y e. A -> -. y e. x ) )
9	8	rexbii	|- ( E. x e. A ( A i^i x ) = (/) <-> E. x e. A A. y ( y e. A -> -. y e. x ) )
10	7 9	e1bi	|- (. A =/= (/) ->. E. x e. A A. y ( y e. A -> -. y e. x ) ).
11		alinexa	|- ( A. y ( y e. A -> -. y e. x ) <-> -. E. y ( y e. A /\ y e. x ) )
12	11	rexbii	|- ( E. x e. A A. y ( y e. A -> -. y e. x ) <-> E. x e. A -. E. y ( y e. A /\ y e. x ) )
13	10 12	e1bi	|- (. A =/= (/) ->. E. x e. A -. E. y ( y e. A /\ y e. x ) ).
14		dfrex2	|- ( E. x e. A -. E. y ( y e. A /\ y e. x ) <-> -. A. x e. A -. -. E. y ( y e. A /\ y e. x ) )
15	13 14	e1bi	|- (. A =/= (/) ->. -. A. x e. A -. -. E. y ( y e. A /\ y e. x ) ).
16		notnotr	|- ( -. -. E. y ( y e. A /\ y e. x ) -> E. y ( y e. A /\ y e. x ) )
17		notnot	|- ( E. y ( y e. A /\ y e. x ) -> -. -. E. y ( y e. A /\ y e. x ) )
18	16 17	impbii	|- ( -. -. E. y ( y e. A /\ y e. x ) <-> E. y ( y e. A /\ y e. x ) )
19	18	ralbii	|- ( A. x e. A -. -. E. y ( y e. A /\ y e. x ) <-> A. x e. A E. y ( y e. A /\ y e. x ) )
20	19	notbii	|- ( -. A. x e. A -. -. E. y ( y e. A /\ y e. x ) <-> -. A. x e. A E. y ( y e. A /\ y e. x ) )
21	15 20	e1bi	|- (. A =/= (/) ->. -. A. x e. A E. y ( y e. A /\ y e. x ) ).
22	21	in1	|- ( A =/= (/) -> -. A. x e. A E. y ( y e. A /\ y e. x ) )