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 4336 | . . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | 1 | necon3abii 3060 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
3 | dfrex2 3237 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitr4i 280 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ≠ wne 3014 ∀wral 3136 ∃wrex 3137 {crab 3140 ∅c0 4289 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-ral 3141 df-rex 3142 df-rab 3145 df-dif 3937 df-nul 4290 |
This theorem is referenced by: class2set 5245 reusv2 5294 exss 5346 frminex 5528 weniso 7099 onminesb 7505 onminsb 7506 onminex 7514 oeeulem 8219 supval2 8911 ordtypelem3 8976 card2on 9010 tz9.12lem3 9210 rankf 9215 scott0 9307 karden 9316 cardf2 9364 cardval3 9373 cardmin2 9419 acni3 9465 kmlem3 9570 cofsmo 9683 coftr 9687 fin23lem7 9730 enfin2i 9735 axcc4 9853 axdc3lem4 9867 ac6num 9893 pwfseqlem3 10074 wuncval 10156 wunccl 10158 tskmcl 10255 infm3 11592 nnwos 12307 zsupss 12329 zmin 12336 rpnnen1lem2 12368 rpnnen1lem1 12369 rpnnen1lem3 12370 rpnnen1lem5 12372 ioo0 12755 ico0 12776 ioc0 12777 icc0 12778 bitsfzolem 15775 lcmcllem 15932 fissn0dvdsn0 15956 odzcllem 16121 vdwnn 16326 ram0 16350 ramsey 16358 sylow2blem3 18739 iscyg2 18993 pgpfac1lem5 19193 ablfaclem2 19200 ablfaclem3 19201 ablfac 19202 lspf 19738 ordtrest2lem 21803 ordthauslem 21983 1stcfb 22045 2ndcdisj 22056 ptclsg 22215 txconn 22289 txflf 22606 tsmsfbas 22728 iscmet3 23888 minveclem3b 24023 iundisj 24141 dyadmax 24191 dyadmbllem 24192 elqaalem1 24900 elqaalem3 24902 sgmnncl 25716 musum 25760 incistruhgr 26856 uvtx01vtx 27171 spancl 29105 shsval2i 29156 ococin 29177 iundisjf 30331 iundisjfi 30511 ordtrest2NEWlem 31158 esumrnmpt2 31320 esumpinfval 31325 dmsigagen 31396 ballotlemfc0 31743 ballotlemfcc 31744 ballotlemiex 31752 ballotlemsup 31755 bnj110 32123 bnj1204 32277 bnj1253 32282 connpconn 32475 iscvm 32499 wsuclem 33105 conway 33257 poimirlem28 34912 sstotbnd2 35044 igenval 35331 igenidl 35333 pmap0 36893 pellfundre 39469 pellfundge 39470 pellfundglb 39473 dgraalem 39736 rgspncl 39760 uzwo4 41306 ioodvbdlimc1lem1 42206 fourierdlem31 42414 fourierdlem64 42446 etransclem48 42558 subsaliuncl 42632 smflimlem6 43043 smfpimcc 43073 prmdvdsfmtnof1lem1 43737 prmdvdsfmtnof 43739 |
Copyright terms: Public domain | W3C validator |