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

Theorem rabbi2dva 3676
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 3450 . 2  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
2 rabbi2dva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  B  <->  ps )
)
32rabbidva 3078 . 2  |-  ( ph  ->  { x  e.  A  |  x  e.  B }  =  { x  e.  A  |  ps } )
41, 3syl5eq 2482 1  |-  ( ph  ->  ( A  i^i  B
)  =  { x  e.  A  |  ps } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   {crab 2786    i^i cin 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-ral 2787  df-rab 2791  df-in 3449
This theorem is referenced by:  fndmdif  6001  bitsshft  14423  sylow3lem2  17215  leordtvallem1  20157  leordtvallem2  20158  ordtt1  20326  xkoccn  20565  txcnmpt  20570  xkopt  20601  ordthmeolem  20747  qustgphaus  21068  itg2monolem1  22585  lhop1  22843  efopn  23468  dirith  24230  pjvec  27184  pjocvec  27185  neibastop3  30803  diarnN  34406
  Copyright terms: Public domain W3C validator