Theorem axacndlem3

Description: Lemma for the Axiom of Choice 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	axacndlem3	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfae	⊢ Ⅎ 𝑧 ∀ 𝑦 𝑦 = 𝑧
2		simpl	⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → 𝑦 ∈ 𝑧 )
3	2	alimi	⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∀ 𝑥 𝑦 ∈ 𝑧 )
4		nd3	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ¬ ∀ 𝑥 𝑦 ∈ 𝑧 )
5	4	pm2.21d	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝑦 ∈ 𝑧 → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
6	3 5	syl5	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
7	1 6	alrimi	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
8	7	axc4i	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
9	8	19.8ad	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )