Metamath Proof Explorer


Theorem ax9ALT

Description: Proof of ax-9 from Tarski's FOL and dfcleq . For a version not using ax-8 either, see eleq2w2 . This shows that dfcleq is too powerful to be used as a definition instead of df-cleq . Note that ax-ext is also a direct consequence of dfcleq (as an instance of its forward implication). (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax9ALT x = y z x z y

Proof

Step Hyp Ref Expression
1 dfcleq x = y t t x t y
2 1 biimpi x = y t t x t y
3 biimp t x t y t x t y
4 2 3 sylg x = y t t x t y
5 ax8 z = t z x t x
6 5 equcoms t = z z x t x
7 ax8 t = z t y z y
8 6 7 imim12d t = z t x t y z x z y
9 8 spimvw t t x t y z x z y
10 4 9 syl x = y z x z y