MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elrabf Unicode version

Theorem elrabf 3255
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.)
Hypotheses
Ref Expression
elrabf.1
elrabf.2
elrabf.3
elrabf.4
Assertion
Ref Expression
elrabf

Proof of Theorem elrabf
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . 3
32adantr 465 . 2
4 df-rab 2816 . . . 4
54eleq2i 2535 . . 3
6 elrabf.1 . . . 4
7 elrabf.2 . . . . . 6
86, 7nfel 2632 . . . . 5
9 elrabf.3 . . . . 5
108, 9nfan 1928 . . . 4
11 eleq1 2529 . . . . 5
12 elrabf.4 . . . . 5
1311, 12anbi12d 710 . . . 4
146, 10, 13elabgf 3244 . . 3
155, 14syl5bb 257 . 2
161, 3, 15pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  F/wnf 1616  e.wcel 1818  {cab 2442  F/_wnfc 2605  {crab 2811   cvv 3109
This theorem is referenced by:  elrab  3257  rabasiun  4334  rabxfrd  4673  onminsb  6634  nnawordex  7305  tskwe  8352  rabssnn0fi  12095  iundisj  21958  iundisjf  27448  iundisjfi  27601  sltval2  29416  nobndlem5  29456  rfcnpre3  31408  rfcnpre4  31409  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem34  31816  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  fourierdlem20  31909  fourierdlem79  31968  bnj1388  34089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111
  Copyright terms: Public domain W3C validator