Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrabf | Structured version Visualization version Unicode version |
Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.) |
Ref | Expression |
---|---|
elrabf.1 | |
elrabf.2 | |
elrabf.3 | |
elrabf.4 |
Ref | Expression |
---|---|
elrabf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3212 | . 2 | |
2 | elex 3212 | . . 3 | |
3 | 2 | adantr 481 | . 2 |
4 | df-rab 2921 | . . . 4 | |
5 | 4 | eleq2i 2693 | . . 3 |
6 | elrabf.1 | . . . 4 | |
7 | elrabf.2 | . . . . . 6 | |
8 | 6, 7 | nfel 2777 | . . . . 5 |
9 | elrabf.3 | . . . . 5 | |
10 | 8, 9 | nfan 1828 | . . . 4 |
11 | eleq1 2689 | . . . . 5 | |
12 | elrabf.4 | . . . . 5 | |
13 | 11, 12 | anbi12d 747 | . . . 4 |
14 | 6, 10, 13 | elabgf 3348 | . . 3 |
15 | 5, 14 | syl5bb 272 | . 2 |
16 | 1, 3, 15 | pm5.21nii 368 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wnf 1708 wcel 1990 cab 2608 wnfc 2751 crab 2916 cvv 3200 |
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-rab 2921 df-v 3202 |
This theorem is referenced by: rabtru 3361 elrab 3363 invdisjrab 4639 rabxfrd 4889 onminsb 6999 nnawordex 7717 tskwe 8776 rabssnn0fi 12785 iundisj 23316 iundisjf 29402 iundisjfi 29555 bnj1388 31101 sltval2 31809 phpreu 33393 poimirlem26 33435 rfcnpre3 39192 rfcnpre4 39193 uzwo4 39221 disjinfi 39380 allbutfiinf 39647 fsumiunss 39807 fnlimfvre 39906 stoweidlem26 40243 stoweidlem27 40244 stoweidlem31 40248 stoweidlem34 40251 stoweidlem51 40268 stoweidlem52 40269 stoweidlem59 40276 fourierdlem20 40344 fourierdlem79 40402 pimdecfgtioc 40925 smfpimcclem 41013 prmdvdsfmtnof1lem1 41496 |
Copyright terms: Public domain | W3C validator |