Theorem axextdfeq

Description: A version of ax-ext for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010)

	Ref	Expression
Assertion	axextdfeq	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axextnd	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
2		ax8	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) )
3	2	imim2i	⊢ ( ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) )
4	1 3	eximii	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) )
5		biimpexp	⊢ ( ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ↔ ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ) )
6	5	exbii	⊢ ( ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ↔ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) ) )
7	4 6	mpbi	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ( ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) → ( 𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤 ) ) )