Metamath Proof Explorer

Theorem axextndbi

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

Ref Expression
Assertion axextndbi ⊢ ∃ z x = y ↔ z ∈ x ↔ z ∈ y

Proof

Step Hyp Ref Expression
1 axextnd ⊢ ∃ z z ∈ x ↔ z ∈ y → x = y
2 elequ2 ⊢ x = y → z ∈ x ↔ z ∈ y
3 2 jctl ⊢ z ∈ x ↔ z ∈ y → x = y → x = y → z ∈ x ↔ z ∈ y ∧ z ∈ x ↔ z ∈ y → x = y
4 1 3 eximii ⊢ ∃ z x = y → z ∈ x ↔ z ∈ y ∧ z ∈ x ↔ z ∈ y → x = y
5 dfbi2 ⊢ x = y ↔ z ∈ x ↔ z ∈ y ↔ x = y → z ∈ x ↔ z ∈ y ∧ z ∈ x ↔ z ∈ y → x = y
6 5 exbii ⊢ ∃ z x = y ↔ z ∈ x ↔ z ∈ y ↔ ∃ z x = y → z ∈ x ↔ z ∈ y ∧ z ∈ x ↔ z ∈ y → x = y
7 4 6 mpbir ⊢ ∃ z x = y ↔ z ∈ x ↔ z ∈ y