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

Theorem elrabf 3196
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 3056 . 2  |-  ( A  e.  { x  e.  B  |  ph }  ->  A  e.  _V )
2 elex 3056 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 467 . 2  |-  ( ( A  e.  B  /\  ps )  ->  A  e. 
_V )
4 df-rab 2748 . . . 4  |-  { x  e.  B  |  ph }  =  { x  |  ( x  e.  B  /\  ph ) }
54eleq2i 2523 . . 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 2606 . . . . 5  |-  F/ x  A  e.  B
9 elrabf.3 . . . . 5  |-  F/ x ps
108, 9nfan 2013 . . . 4  |-  F/ x
( A  e.  B  /\  ps )
11 eleq1 2519 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
12 elrabf.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
1311, 12anbi12d 718 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  /\  ph )  <->  ( A  e.  B  /\  ps )
) )
146, 10, 13elabgf 3185 . . 3  |-  ( A  e.  _V  ->  ( A  e.  { x  |  ( x  e.  B  /\  ph ) } 
<->  ( A  e.  B  /\  ps ) ) )
155, 14syl5bb 261 . 2  |-  ( A  e.  _V  ->  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) ) )
161, 3, 15pm5.21nii 355 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446   F/wnf 1669    e. wcel 1889   {cab 2439   F/_wnfc 2581   {crab 2743   _Vcvv 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-rab 2748  df-v 3049
This theorem is referenced by:  elrab  3198  rabasiun  4285  invdisjrab  4395  rabxfrd  4624  onminsb  6631  nnawordex  7343  tskwe  8389  rabssnn0fi  12205  iundisj  22513  rabtru  28147  iundisjf  28211  iundisjfi  28384  bnj1388  29854  sltval2  30555  nobndlem5  30597  phpreu  31941  poimirlem26  31978  rfcnpre3  37364  rfcnpre4  37365  uzwo4  37402  disjinfi  37478  fsumiunss  37664  stoweidlem26  37896  stoweidlem27  37897  stoweidlem31  37902  stoweidlem34  37905  stoweidlem51  37922  stoweidlem52  37923  stoweidlem59  37930  fourierdlem20  37999  fourierdlem79  38059
  Copyright terms: Public domain W3C validator