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

Theorem 19.42v 1848
Description: Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.42v  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem 19.42v
StepHypRef Expression
1 nfv 1606 . 2  |-  F/ x ph
2119.42 1818 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1529
This theorem is referenced by:  exdistr  1849  19.42vv  1850  19.42vvv  1851  4exdistr  1854  cbvex2  1951  2sb5  2055  2sb5rf  2060  rexcom4a  2810  ceqsex2  2826  reuind  2970  2reu5lem3  2974  sbccomlem  3063  bm1.3ii  4146  eqvinop  4251  uniuni  4527  dmopabss  4890  dmopab3  4891  mptpreima  5165  fndmin  5594  zfrep6  5710  opabex3  5731  fliftf  5776  dfoprab2  5857  dmoprab  5890  dmoprabss  5891  fnoprabg  5907  fsplit  6185  eroveu  6749  rankuni  7531  aceq1  7740  dfac3  7744  kmlem14  7785  kmlem15  7786  axdc2lem  8070  1idpr  8649  ltexprlem1  8656  ltexprlem4  8659  shftdm  11561  ntreq0  16809  adjeu  22462  dfiota3  23870  eqvinopb  24364  copsexgb  24365  dmoprabss6  24434  cmppar2  25372  pm11.58  26989  pm11.71  26996  2sbc5g  27016  iotasbc2  27020  stoweidlem60  27209  a9e2nd  27596  a9e2ndVD  27953  a9e2ndALT  27976  bnj1019  28079  bnj1209  28097  bnj1033  28267  bnj1189  28307
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator