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

Theorem rabbi2dva 3570
Description: Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.)
Hypothesis
Ref Expression
rabbi2dva.1  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  B  <->  ps )
)
Assertion
Ref Expression
rabbi2dva  |-  ( ph  ->  ( A  i^i  B
)  =  { x  e.  A  |  ps } )
Distinct variable groups:    ph, x    x, A    x, B
Allowed substitution hint:    ps( x)

Proof of Theorem rabbi2dva
StepHypRef Expression
1 dfin5 3348 . 2  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
2 rabbi2dva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  B  <->  ps )
)
32rabbidva 2975 . 2  |-  ( ph  ->  { x  e.  A  |  x  e.  B }  =  { x  e.  A  |  ps } )
41, 3syl5eq 2487 1  |-  ( ph  ->  ( A  i^i  B
)  =  { x  e.  A  |  ps } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   {crab 2731    i^i cin 3339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-ral 2732  df-rab 2736  df-in 3347
This theorem is referenced by:  fndmdif  5819  bitsshft  13683  sylow3lem2  16139  leordtvallem1  18826  leordtvallem2  18827  ordtt1  18995  xkoccn  19204  txcnmpt  19209  xkopt  19240  ordthmeolem  19386  divstgphaus  19705  itg2monolem1  21240  lhop1  21498  efopn  22115  dirith  22790  pjvec  25111  pjocvec  25112  neibastop3  28595  diarnN  34786
  Copyright terms: Public domain W3C validator