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

Theorem elrabf 3034
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  |-  F/_ x A
elrabf.2  |-  F/_ x B
elrabf.3  |-  F/ x ps
elrabf.4  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
elrabf  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )

Proof of Theorem elrabf
StepHypRef Expression
1 elex 2907 . 2  |-  ( A  e.  { x  e.  B  |  ph }  ->  A  e.  _V )
2 elex 2907 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 452 . 2  |-  ( ( A  e.  B  /\  ps )  ->  A  e. 
_V )
4 df-rab 2658 . . . 4  |-  { x  e.  B  |  ph }  =  { x  |  ( x  e.  B  /\  ph ) }
54eleq2i 2451 . . 3  |-  ( A  e.  { x  e.  B  |  ph }  <->  A  e.  { x  |  ( x  e.  B  /\  ph ) } )
6 elrabf.1 . . . 4  |-  F/_ x A
7 elrabf.2 . . . . . 6  |-  F/_ x B
86, 7nfel 2531 . . . . 5  |-  F/ x  A  e.  B
9 elrabf.3 . . . . 5  |-  F/ x ps
108, 9nfan 1836 . . . 4  |-  F/ x
( A  e.  B  /\  ps )
11 eleq1 2447 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
12 elrabf.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
1311, 12anbi12d 692 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  /\  ph )  <->  ( A  e.  B  /\  ps )
) )
146, 10, 13elabgf 3023 . . 3  |-  ( A  e.  _V  ->  ( A  e.  { x  |  ( x  e.  B  /\  ph ) } 
<->  ( A  e.  B  /\  ps ) ) )
155, 14syl5bb 249 . 2  |-  ( A  e.  _V  ->  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) ) )
161, 3, 15pm5.21nii 343 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   F/wnf 1550    = wceq 1649    e. wcel 1717   {cab 2373   F/_wnfc 2510   {crab 2653   _Vcvv 2899
This theorem is referenced by:  elrab  3035  rabxfrd  4684  onminsb  4719  nnawordex  6816  tskwe  7770  iundisj  19309  iundisjf  23872  iundisjfi  23990  sltval2  25334  nobndlem5  25374  rfcnpre3  27372  rfcnpre4  27373  stoweidlem26  27443  stoweidlem27  27444  stoweidlem31  27448  stoweidlem34  27451  stoweidlem51  27468  stoweidlem52  27469  stoweidlem59  27476  bnj1388  28740
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rab 2658  df-v 2901
  Copyright terms: Public domain W3C validator