Theorem axextndbi

Description: axextnd as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010)

	Ref	Expression
Assertion	axextndbi	⊢ ∃ 𝑧 ( 𝑥 = 𝑦 ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		axextnd	⊢ ∃ 𝑧 ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 )
2		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
3	2	jctl	⊢ ( ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) → ( ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
4	1 3	eximii	⊢ ∃ 𝑧 ( ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
5		dfbi2	⊢ ( ( 𝑥 = 𝑦 ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ↔ ( ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
6	5	exbii	⊢ ( ∃ 𝑧 ( 𝑥 = 𝑦 ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ↔ ∃ 𝑧 ( ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ∧ ( ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
7	4 6	mpbir	⊢ ∃ 𝑧 ( 𝑥 = 𝑦 ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )