Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Scott Fenton
Defined equality axioms
axextndbi
Next ⟩
Hypothesis builders
Metamath Proof Explorer
Ascii
Unicode
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