![]() |
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 4349 | . . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
2 | 1 | necon3abii 2991 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
3 | dfrex2 3077 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑) | |
4 | 2, 3 | bitr4i 278 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ≠ wne 2944 ∀wral 3065 ∃wrex 3074 {crab 3410 ∅c0 4287 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2715 df-cleq 2729 df-ne 2945 df-ral 3066 df-rex 3075 df-rab 3411 df-dif 3918 df-nul 4288 |
This theorem is referenced by: class2set 5315 reusv2 5363 exss 5425 frminex 5618 weniso 7304 onminesb 7733 onminsb 7734 onminex 7742 oeeulem 8553 supval2 9398 ordtypelem3 9463 card2on 9497 tz9.12lem3 9732 rankf 9737 scott0 9829 karden 9838 cardf2 9886 cardval3 9895 cardmin2 9942 acni3 9990 kmlem3 10095 cofsmo 10212 coftr 10216 fin23lem7 10259 enfin2i 10264 axcc4 10382 axdc3lem4 10396 ac6num 10422 pwfseqlem3 10603 wuncval 10685 wunccl 10687 tskmcl 10784 infm3 12121 nnwos 12847 zsupss 12869 zmin 12876 rpnnen1lem2 12909 rpnnen1lem1 12910 rpnnen1lem3 12911 rpnnen1lem5 12913 ioo0 13296 ico0 13317 ioc0 13318 icc0 13319 bitsfzolem 16321 lcmcllem 16479 fissn0dvdsn0 16503 odzcllem 16671 vdwnn 16877 ram0 16901 ramsey 16909 sylow2blem3 19411 iscyg2 19666 pgpfac1lem5 19865 ablfaclem2 19872 ablfaclem3 19873 ablfac 19874 lspf 20451 ordtrest2lem 22570 ordthauslem 22750 1stcfb 22812 2ndcdisj 22823 ptclsg 22982 txconn 23056 txflf 23373 tsmsfbas 23495 iscmet3 24673 minveclem3b 24808 iundisj 24928 dyadmax 24978 dyadmbllem 24979 elqaalem1 25695 elqaalem3 25697 sgmnncl 26512 musum 26556 conway 27160 incistruhgr 28072 uvtx01vtx 28387 spancl 30320 shsval2i 30371 ococin 30392 iundisjf 31549 iundisjfi 31741 ordtrest2NEWlem 32543 esumrnmpt2 32707 esumpinfval 32712 dmsigagen 32783 ballotlemfc0 33132 ballotlemfcc 33133 ballotlemiex 33141 ballotlemsup 33144 bnj110 33510 bnj1204 33664 bnj1253 33669 connpconn 33869 iscvm 33893 wsuclem 34439 poimirlem28 36135 sstotbnd2 36262 igenval 36549 igenidl 36551 pmap0 38257 aks4d1p4 40565 aks4d1p5 40566 aks4d1p7 40569 aks4d1p8 40573 fsuppind 40794 pellfundre 41233 pellfundge 41234 pellfundglb 41237 dgraalem 41501 rgspncl 41525 uzwo4 43335 ioodvbdlimc1lem1 44246 fourierdlem31 44453 fourierdlem64 44485 etransclem48 44597 subsaliuncl 44673 smflimlem6 45091 smfpimcc 45123 prmdvdsfmtnof1lem1 45850 prmdvdsfmtnof 45852 |
Copyright terms: Public domain | W3C validator |