Metamath Proof Explorer


Theorem nfmod2

Description: Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . See nfmodv for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) Avoid df-eu . (Revised by BJ, 14-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses nfmod2.1 y φ
nfmod2.2 φ ¬ x x = y x ψ
Assertion nfmod2 φ x * y ψ

Proof

Step Hyp Ref Expression
1 nfmod2.1 y φ
2 nfmod2.2 φ ¬ x x = y x ψ
3 df-mo * y ψ z y ψ y = z
4 nfv z φ
5 nfeqf1 ¬ x x = y x y = z
6 5 adantl φ ¬ x x = y x y = z
7 2 6 nfimd φ ¬ x x = y x ψ y = z
8 1 7 nfald2 φ x y ψ y = z
9 4 8 nfexd φ x z y ψ y = z
10 3 9 nfxfrd φ x * y ψ