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

Theorem elrabf 3222
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 3087 . 2  |-  ( A  e.  { x  e.  B  |  ph }  ->  A  e.  _V )
2 elex 3087 . . 3  |-  ( A  e.  B  ->  A  e.  _V )
32adantr 465 . 2  |-  ( ( A  e.  B  /\  ps )  ->  A  e. 
_V )
4 df-rab 2808 . . . 4  |-  { x  e.  B  |  ph }  =  { x  |  ( x  e.  B  /\  ph ) }
54eleq2i 2532 . . 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 2629 . . . . 5  |-  F/ x  A  e.  B
9 elrabf.3 . . . . 5  |-  F/ x ps
108, 9nfan 1866 . . . 4  |-  F/ x
( A  e.  B  /\  ps )
11 eleq1 2526 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
12 elrabf.4 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
1311, 12anbi12d 710 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  /\  ph )  <->  ( A  e.  B  /\  ps )
) )
146, 10, 13elabgf 3211 . . 3  |-  ( A  e.  _V  ->  ( A  e.  { x  |  ( x  e.  B  /\  ph ) } 
<->  ( A  e.  B  /\  ps ) ) )
155, 14syl5bb 257 . 2  |-  ( A  e.  _V  ->  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) ) )
161, 3, 15pm5.21nii 353 1  |-  ( A  e.  { x  e.  B  |  ph }  <->  ( A  e.  B  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370   F/wnf 1590    e. wcel 1758   {cab 2439   F/_wnfc 2602   {crab 2803   _Vcvv 3078
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080
This theorem is referenced by:  elrab  3224  rabxfrd  4624  onminsb  6523  nnawordex  7189  tskwe  8234  iundisj  21165  iundisjf  26102  iundisjfi  26245  sltval2  27961  nobndlem5  28001  rfcnpre3  29923  rfcnpre4  29924  stoweidlem26  29989  stoweidlem27  29990  stoweidlem31  29994  stoweidlem34  29997  stoweidlem51  30014  stoweidlem52  30015  stoweidlem59  30022  rabasiun  30398  rabssnn0fi  30915  bnj1388  32376
  Copyright terms: Public domain W3C validator