New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > mobii | Unicode version |
Description: Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) |
Ref | Expression |
---|---|
mobii.1 |
Ref | Expression |
---|---|
mobii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mobii.1 | . . . 4 | |
2 | 1 | a1i 10 | . . 3 |
3 | 2 | mobidv 2239 | . 2 |
4 | 3 | trud 1323 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wtru 1316 wmo 2205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-tru 1319 df-ex 1542 df-nf 1545 df-eu 2208 df-mo 2209 |
This theorem is referenced by: moaneu 2263 moanmo 2264 2moswap 2279 2eu1 2284 rmobiia 2801 rmov 2875 euxfr2 3021 rmoan 3034 2reu5lem2 3042 dffun9 5135 funopab 5139 funsn 5147 funcnv2 5155 funcnv 5156 fncnv 5158 imadif 5171 fnres 5199 ov3 5599 |
Copyright terms: Public domain | W3C validator |