Theorem 2ax6eOLD

Description: Obsolete version of 2ax6e as of 3-Oct-2023. (Contributed by Wolf Lammen, 28-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2ax6eOLD	⊢ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		aeveq	⊢ ( ∀ 𝑤 𝑤 = 𝑧 → 𝑧 = 𝑥 )
2		aeveq	⊢ ( ∀ 𝑤 𝑤 = 𝑧 → 𝑤 = 𝑦 )
3	1 2	jca	⊢ ( ∀ 𝑤 𝑤 = 𝑧 → ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
4		19.8a	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
5		19.8a	⊢ ( ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
6	3 4 5	3syl	⊢ ( ∀ 𝑤 𝑤 = 𝑧 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
7		2ax6elem	⊢ ( ¬ ∀ 𝑤 𝑤 = 𝑧 → ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
8	6 7	pm2.61i	⊢ ∃ 𝑧 ∃ 𝑤 ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 )