![]() |
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 4185 | . . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | 1 | necon3abii 3044 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
3 | dfrex2 3203 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ≠ wne 2998 ∀wral 3116 ∃wrex 3117 {crab 3120 ∅c0 4143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-dif 3800 df-nul 4144 |
This theorem is referenced by: class2set 5053 reusv2 5102 exss 5151 frminex 5321 weniso 6858 onminesb 7258 onminsb 7259 onminex 7267 oeeulem 7947 supval2 8629 ordtypelem3 8693 card2on 8727 tz9.12lem3 8928 rankf 8933 scott0 9025 karden 9034 cardf2 9081 cardval3 9090 cardmin2 9136 acni3 9182 kmlem3 9288 cofsmo 9405 coftr 9409 fin23lem7 9452 enfin2i 9457 axcc4 9575 axdc3lem4 9589 ac6num 9615 pwfseqlem3 9796 wuncval 9878 wunccl 9880 tskmcl 9977 infm3 11311 nnwos 12037 zsupss 12059 zmin 12066 rpnnen1lem2 12098 rpnnen1lem1 12099 rpnnen1lem3 12100 rpnnen1lem5 12102 ioo0 12487 ico0 12508 ioc0 12509 icc0 12510 bitsfzolem 15528 lcmcllem 15681 fissn0dvdsn0 15705 odzcllem 15867 vdwnn 16072 ram0 16096 ramsey 16104 sylow2blem3 18387 iscyg2 18636 pgpfac1lem5 18831 ablfaclem2 18838 ablfaclem3 18839 ablfac 18840 lspf 19332 ordtrest2lem 21377 ordthauslem 21557 1stcfb 21618 2ndcdisj 21629 ptclsg 21788 txconn 21862 txflf 22179 tsmsfbas 22300 iscmet3 23460 minveclem3b 23595 iundisj 23713 dyadmax 23763 dyadmbllem 23764 elqaalem1 24472 elqaalem3 24474 sgmnncl 25285 musum 25329 incistruhgr 26376 uvtx01vtx 26694 spancl 28749 shsval2i 28800 ococin 28821 iundisjf 29948 iundisjfi 30101 ordtrest2NEWlem 30512 esumrnmpt2 30674 esumpinfval 30679 dmsigagen 30751 ballotlemfc0 31099 ballotlemfcc 31100 ballotlemiex 31108 ballotlemsup 31111 bnj110 31473 bnj1204 31625 bnj1253 31630 connpconn 31762 iscvm 31786 wsuclem 32308 conway 32448 poimirlem28 33980 sstotbnd2 34114 igenval 34401 igenidl 34403 pmap0 35839 pellfundre 38288 pellfundge 38289 pellfundglb 38292 dgraalem 38557 rgspncl 38581 uzwo4 40037 ioodvbdlimc1lem1 40940 fourierdlem31 41148 fourierdlem64 41180 etransclem48 41292 subsaliuncl 41366 smflimlem6 41777 smfpimcc 41807 prmdvdsfmtnof1lem1 42325 prmdvdsfmtnof 42327 |
Copyright terms: Public domain | W3C validator |