Metamath Proof Explorer


Theorem ax13lem2

Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)

Ref Expression
Assertion ax13lem2 ¬x=yxz=yz=y

Proof

Step Hyp Ref Expression
1 ax13lem1 ¬x=yw=yxw=y
2 equeucl z=yw=yz=w
3 2 eximi xz=yxw=yz=w
4 19.36v xw=yz=wxw=yz=w
5 3 4 sylib xz=yxw=yz=w
6 1 5 syl9 ¬x=yxz=yw=yz=w
7 6 alrimdv ¬x=yxz=yww=yz=w
8 equequ2 w=yz=wz=y
9 8 equsalvw ww=yz=wz=y
10 7 9 imbitrdi ¬x=yxz=yz=y