Metamath Proof Explorer


Theorem wl-mo2tf

Description: Closed form of mof with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020)

Ref Expression
Assertion wl-mo2tf ¬ x x = y x y φ * x φ y x φ x = y

Proof

Step Hyp Ref Expression
1 nfnae x ¬ x x = y
2 nfa1 x x y φ
3 1 2 nfan x ¬ x x = y x y φ
4 nfnae y ¬ x x = y
5 nfnf1 y y φ
6 5 nfal y x y φ
7 4 6 nfan y ¬ x x = y x y φ
8 simpl ¬ x x = y x y φ ¬ x x = y
9 sp x y φ y φ
10 9 adantl ¬ x x = y x y φ y φ
11 3 7 8 10 wl-mo2df ¬ x x = y x y φ * x φ y x φ x = y