Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexrab | Structured version Visualization version Unicode version |
Description: Existential quantification over a class abstraction. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Ref | Expression |
---|---|
ralab.1 |
Ref | Expression |
---|---|
rexrab |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralab.1 | . . . . 5 | |
2 | 1 | elrab 3363 | . . . 4 |
3 | 2 | anbi1i 731 | . . 3 |
4 | anass 681 | . . 3 | |
5 | 3, 4 | bitri 264 | . 2 |
6 | 5 | rexbii2 3039 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wcel 1990 wrex 2913 crab 2916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-rab 2921 df-v 3202 |
This theorem is referenced by: wereu2 5111 wdom2d 8485 enfin2i 9143 infm3 10982 pmtrfrn 17878 pgpssslw 18029 ellspd 20141 1stcfb 21248 xkobval 21389 xkococn 21463 imasdsf1olem 22178 rusgrnumwwlks 26869 cvmliftlem15 31280 wsuclem 31773 wsuclemOLD 31774 scutun12 31917 poimirlem4 33413 poimirlem26 33435 poimirlem27 33436 rexrabdioph 37358 hbtlem6 37699 |
Copyright terms: Public domain | W3C validator |