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