# Metamath Proof Explorer

## Theorem axextdfeq

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

Ref Expression
Assertion axextdfeq ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}\to {z}\in {y}\right)\to \left(\left({z}\in {y}\to {z}\in {x}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 axextnd ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}↔{z}\in {y}\right)\to {x}={y}\right)$
2 ax8 ${⊢}{x}={y}\to \left({x}\in {w}\to {y}\in {w}\right)$
3 2 imim2i ${⊢}\left(\left({z}\in {x}↔{z}\in {y}\right)\to {x}={y}\right)\to \left(\left({z}\in {x}↔{z}\in {y}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)$
4 1 3 eximii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}↔{z}\in {y}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)$
5 biimpexp ${⊢}\left(\left({z}\in {x}↔{z}\in {y}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)↔\left(\left({z}\in {x}\to {z}\in {y}\right)\to \left(\left({z}\in {y}\to {z}\in {x}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)\right)$
6 5 exbii ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}↔{z}\in {y}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)↔\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}\to {z}\in {y}\right)\to \left(\left({z}\in {y}\to {z}\in {x}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)\right)$
7 4 6 mpbi ${⊢}\exists {z}\phantom{\rule{.4em}{0ex}}\left(\left({z}\in {x}\to {z}\in {y}\right)\to \left(\left({z}\in {y}\to {z}\in {x}\right)\to \left({x}\in {w}\to {y}\in {w}\right)\right)\right)$