Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nrex | Structured version Visualization version Unicode version |
Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) |
Ref | Expression |
---|---|
nrex.1 |
Ref | Expression |
---|---|
nrex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nrex.1 | . . 3 | |
2 | 1 | rgen 2922 | . 2 |
3 | ralnex 2992 | . 2 | |
4 | 2, 3 | mpbi 220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wcel 1990 wral 2912 wrex 2913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-ral 2917 df-rex 2918 |
This theorem is referenced by: rex0 3938 iun0 4576 canth 6608 orduninsuc 7043 wfrlem16 7430 wofib 8450 cfsuc 9079 nominpos 11269 nnunb 11288 indstr 11756 eirr 14933 sqrt2irr 14979 vdwap0 15680 psgnunilem3 17916 bwth 21213 zfbas 21700 aaliou3lem9 24105 vma1 24892 hatomistici 29221 esumrnmpt2 30130 linedegen 32250 limsucncmpi 32444 elpadd0 35095 fourierdlem62 40385 etransc 40500 0nodd 41810 2nodd 41812 1neven 41932 |
Copyright terms: Public domain | W3C validator |