Theorem zfreg 8115

Description: The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring] p. 21. This is called the "weak form." There is also a "strong form," not requiring that A be a set, that can be proved with more difficulty (see zfregs 8221). (Contributed by NM, 26-Nov-1995.)

Hypothesis

Ref	Expression
zfreg.1	|- A e. _V

Assertion

Ref	Expression
zfreg	|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )

Distinct variable group:   x, A

Proof of Theorem zfreg

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfreg.1	. . 3 |- A e. _V
2	1	zfregcl 8114	. 2 |- ( E. x x e. A -> E. x e. A A. y e. x -. y e. A )
3		n0 3743	. 2 |- ( A =/= (/) <-> E. x x e. A )
4		disj 3807	. . 3 |- ( ( x i^i A ) = (/) <-> A. y e. x -. y e. A )
5	4	rexbii 2891	. 2 |- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A A. y e. x -. y e. A )
6	2, 3, 5	3imtr4i 270	1 |- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1446   E.wex 1665   e. wcel 1889   =/= wne 2624   A.wral 2739   E.wrex 2740   _Vcvv 3047   i^i cin 3405   (/)c0 3733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-reg 8112

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-v 3049  df-dif 3409  df-in 3413  df-nul 3734

This theorem is referenced by:  en3lp  8126  inf3lem3  8140  setindtr  35891