Theorem axregndlem1

Description: Lemma for the Axiom of Regularity with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Jan-2002) (New usage is discouraged.)

	Ref	Expression
Assertion	axregndlem1	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		19.8a	⊢ ( 𝑥 ∈ 𝑦 → ∃ 𝑥 𝑥 ∈ 𝑦 )
2		nfae	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑧
3		nfae	⊢ Ⅎ 𝑧 ∀ 𝑥 𝑥 = 𝑧
4		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
5		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
6	4 5	mtbii	⊢ ( 𝑥 = 𝑧 → ¬ 𝑧 ∈ 𝑥 )
7	6	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ¬ 𝑧 ∈ 𝑥 )
8	7	pm2.21d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
9	3 8	alrimi	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) )
10	9	anim2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 𝑥 = 𝑧 ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) )
11	10	expcom	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
12	2 11	eximd	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )
13	1 12	syl5	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦 ) ) ) )