Metamath Proof Explorer


Theorem zfreg

Description: The Axiom of Regularity using abbreviations. Axiom 6 of TakeutiZaring p. 21. This is called the "weak form". Axiom Reg of BellMachover p. 480. There is also a "strong form", not requiring that A be a set, that can be proved with more difficulty (see zfregs ). (Contributed by NM, 26-Nov-1995) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021)

Ref Expression
Assertion zfreg ( ( 𝐴𝑉𝐴 ≠ ∅ ) → ∃ 𝑥𝐴 ( 𝑥𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 n0 ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐴 )
2 1 biimpi ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥𝐴 )
3 2 anim2i ( ( 𝐴𝑉𝐴 ≠ ∅ ) → ( 𝐴𝑉 ∧ ∃ 𝑥 𝑥𝐴 ) )
4 zfregcl ( 𝐴𝑉 → ( ∃ 𝑥 𝑥𝐴 → ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝐴 ) )
5 4 imp ( ( 𝐴𝑉 ∧ ∃ 𝑥 𝑥𝐴 ) → ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝐴 )
6 disj ( ( 𝑥𝐴 ) = ∅ ↔ ∀ 𝑦𝑥 ¬ 𝑦𝐴 )
7 6 rexbii ( ∃ 𝑥𝐴 ( 𝑥𝐴 ) = ∅ ↔ ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝐴 )
8 7 biimpri ( ∃ 𝑥𝐴𝑦𝑥 ¬ 𝑦𝐴 → ∃ 𝑥𝐴 ( 𝑥𝐴 ) = ∅ )
9 3 5 8 3syl ( ( 𝐴𝑉𝐴 ≠ ∅ ) → ∃ 𝑥𝐴 ( 𝑥𝐴 ) = ∅ )