This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝑥 ∩ 𝐴 ) = ∅ )