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

Theorem rabbi2dva 3390
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 3173 . 2  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
2 rabbi2dva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  (
x  e.  B  <->  ps )
)
32rabbidva 2792 . 2  |-  ( ph  ->  { x  e.  A  |  x  e.  B }  =  { x  e.  A  |  ps } )
41, 3syl5eq 2340 1  |-  ( ph  ->  ( A  i^i  B
)  =  { x  e.  A  |  ps } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   {crab 2560    i^i cin 3164
This theorem is referenced by:  fndmdif  5645  bitsshft  12682  sylow3lem2  14955  leordtvallem1  16956  leordtvallem2  16957  ordtt1  17123  xkoccn  17329  txcnmpt  17334  xkopt  17365  ordthmeolem  17508  divstgphaus  17821  itg2monolem1  19121  lhop1  19377  efopn  20021  dirith  20694  pjvec  22291  pjocvec  22292  neibastop3  26414  diarnN  31941
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-ral 2561  df-rab 2565  df-in 3172
  Copyright terms: Public domain W3C validator