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

Theorem 19.42v 2038
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 1629 . 2  |-  F/ x ph
2119.42 1800 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537
This theorem is referenced by:  exdistr  2039  19.42vv  2040  19.42vvv  2041  4exdistr  2044  cbvex2  2048  2sb5  2072  2sb5rf  2077  rexcom4a  2746  ceqsex2  2762  reuind  2903  sbccomlem  2991  bm1.3ii  4041  eqvinop  4144  uniuni  4418  dmopabss  4797  dmopab3  4798  mptpreima  5072  fndmin  5484  zfrep6  5600  opabex3  5621  fliftf  5666  dfoprab2  5747  dmoprab  5780  dmoprabss  5781  fnoprabg  5797  fsplit  6075  eroveu  6639  rankuni  7419  aceq1  7628  dfac3  7632  kmlem14  7673  kmlem15  7674  axdc2lem  7958  1idpr  8533  ltexprlem1  8540  ltexprlem4  8543  shftdm  11443  ntreq0  16646  adjeu  22299  dfiota3  23636  eqvinopb  24130  copsexgb  24131  dmoprabss6  24200  cmppar2  25138  pm11.58  26755  pm11.71  26762  2sbc5g  26783  iotasbc2  26787  a9e2nd  27017  a9e2ndVD  27374  a9e2ndALT  27397  bnj1019  27500  bnj1209  27518  bnj1033  27688  bnj1189  27728
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator