Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabn0 | Structured version Visualization version GIF version |
Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.) |
Ref | Expression |
---|---|
rabn0 | ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeq0 4337 | . . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | 1 | necon3abii 3062 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
3 | dfrex2 3239 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitr4i 279 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 {crab 3142 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-dif 3938 df-nul 4291 |
This theorem is referenced by: class2set 5246 reusv2 5295 exss 5347 frminex 5529 weniso 7096 onminesb 7501 onminsb 7502 onminex 7510 oeeulem 8217 supval2 8908 ordtypelem3 8973 card2on 9007 tz9.12lem3 9207 rankf 9212 scott0 9304 karden 9313 cardf2 9361 cardval3 9370 cardmin2 9416 acni3 9462 kmlem3 9567 cofsmo 9680 coftr 9684 fin23lem7 9727 enfin2i 9732 axcc4 9850 axdc3lem4 9864 ac6num 9890 pwfseqlem3 10071 wuncval 10153 wunccl 10155 tskmcl 10252 infm3 11589 nnwos 12304 zsupss 12326 zmin 12333 rpnnen1lem2 12366 rpnnen1lem1 12367 rpnnen1lem3 12368 rpnnen1lem5 12370 ioo0 12753 ico0 12774 ioc0 12775 icc0 12776 bitsfzolem 15773 lcmcllem 15930 fissn0dvdsn0 15954 odzcllem 16119 vdwnn 16324 ram0 16348 ramsey 16356 sylow2blem3 18678 iscyg2 18932 pgpfac1lem5 19132 ablfaclem2 19139 ablfaclem3 19140 ablfac 19141 lspf 19677 ordtrest2lem 21741 ordthauslem 21921 1stcfb 21983 2ndcdisj 21994 ptclsg 22153 txconn 22227 txflf 22544 tsmsfbas 22665 iscmet3 23825 minveclem3b 23960 iundisj 24078 dyadmax 24128 dyadmbllem 24129 elqaalem1 24837 elqaalem3 24839 sgmnncl 25652 musum 25696 incistruhgr 26792 uvtx01vtx 27107 spancl 29041 shsval2i 29092 ococin 29113 iundisjf 30268 iundisjfi 30446 ordtrest2NEWlem 31065 esumrnmpt2 31227 esumpinfval 31232 dmsigagen 31303 ballotlemfc0 31650 ballotlemfcc 31651 ballotlemiex 31659 ballotlemsup 31662 bnj110 32030 bnj1204 32182 bnj1253 32187 connpconn 32380 iscvm 32404 wsuclem 33010 conway 33162 poimirlem28 34802 sstotbnd2 34935 igenval 35222 igenidl 35224 pmap0 36783 pellfundre 39358 pellfundge 39359 pellfundglb 39362 dgraalem 39625 rgspncl 39649 uzwo4 41195 ioodvbdlimc1lem1 42096 fourierdlem31 42304 fourierdlem64 42336 etransclem48 42448 subsaliuncl 42522 smflimlem6 42933 smfpimcc 42963 prmdvdsfmtnof1lem1 43593 prmdvdsfmtnof 43595 |
Copyright terms: Public domain | W3C validator |