![]() |
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 4384 | . . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | 1 | necon3abii 2986 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
3 | dfrex2 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitr4i 278 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 {crab 3431 ∅c0 4322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-dif 3951 df-nul 4323 |
This theorem is referenced by: class2set 5353 reusv2 5401 exss 5463 frminex 5656 weniso 7354 onminesb 7785 onminsb 7786 onminex 7794 oeeulem 8605 supval2 9454 ordtypelem3 9519 card2on 9553 tz9.12lem3 9788 rankf 9793 scott0 9885 karden 9894 cardf2 9942 cardval3 9951 cardmin2 9998 acni3 10046 kmlem3 10151 cofsmo 10268 coftr 10272 fin23lem7 10315 enfin2i 10320 axcc4 10438 axdc3lem4 10452 ac6num 10478 pwfseqlem3 10659 wuncval 10741 wunccl 10743 tskmcl 10840 infm3 12178 nnwos 12904 zsupss 12926 zmin 12933 rpnnen1lem2 12966 rpnnen1lem1 12967 rpnnen1lem3 12968 rpnnen1lem5 12970 ioo0 13354 ico0 13375 ioc0 13376 icc0 13377 bitsfzolem 16380 lcmcllem 16538 fissn0dvdsn0 16562 odzcllem 16730 vdwnn 16936 ram0 16960 ramsey 16968 sylow2blem3 19532 iscyg2 19792 pgpfac1lem5 19991 ablfaclem2 19998 ablfaclem3 19999 ablfac 20000 lspf 20730 ordtrest2lem 22928 ordthauslem 23108 1stcfb 23170 2ndcdisj 23181 ptclsg 23340 txconn 23414 txflf 23731 tsmsfbas 23853 iscmet3 25042 minveclem3b 25177 iundisj 25298 dyadmax 25348 dyadmbllem 25349 elqaalem1 26069 elqaalem3 26071 sgmnncl 26888 musum 26932 conway 27538 incistruhgr 28607 uvtx01vtx 28922 spancl 30857 shsval2i 30908 ococin 30929 iundisjf 32088 iundisjfi 32275 ordtrest2NEWlem 33201 esumrnmpt2 33365 esumpinfval 33370 dmsigagen 33441 ballotlemfc0 33790 ballotlemfcc 33791 ballotlemiex 33799 ballotlemsup 33802 bnj110 34168 bnj1204 34322 bnj1253 34327 connpconn 34525 iscvm 34549 wsuclem 35102 poimirlem28 36820 sstotbnd2 36946 igenval 37233 igenidl 37235 pmap0 38940 aks4d1p4 41251 aks4d1p5 41252 aks4d1p7 41255 aks4d1p8 41259 fsuppind 41465 pellfundre 41922 pellfundge 41923 pellfundglb 41926 dgraalem 42190 rgspncl 42214 uzwo4 44042 ioodvbdlimc1lem1 44946 fourierdlem31 45153 fourierdlem64 45185 etransclem48 45297 subsaliuncl 45373 smflimlem6 45791 smfpimcc 45823 prmdvdsfmtnof1lem1 46551 prmdvdsfmtnof 46553 |
Copyright terms: Public domain | W3C validator |