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