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 | ||
nfmod2.2 | |||
Assertion | nfmod2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfmod2.1 | ||
2 | nfmod2.2 | ||
3 | df-mo | ||
4 | nfv | ||
5 | nfeqf1 | ||
6 | 5 | adantl | |
7 | 2 6 | nfimd | |
8 | 1 7 | nfald2 | |
9 | 4 8 | nfexd | |
10 | 3 9 | nfxfrd |