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

Theorem 19.42v 2039
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  2040  19.42vv  2041  19.42vvv  2042  4exdistr  2045  cbvex2  2049  2sb5  2075  2sb5rf  2080  rexcom4a  2759  ceqsex2  2775  reuind  2917  sbccomlem  3005  bm1.3ii  4084  eqvinop  4188  uniuni  4464  dmopabss  4843  dmopab3  4844  mptpreima  5118  fndmin  5531  zfrep6  5647  opabex3  5668  fliftf  5713  dfoprab2  5794  dmoprab  5827  dmoprabss  5828  fnoprabg  5844  fsplit  6122  eroveu  6686  rankuni  7468  aceq1  7677  dfac3  7681  kmlem14  7722  kmlem15  7723  axdc2lem  8007  1idpr  8586  ltexprlem1  8593  ltexprlem4  8596  shftdm  11496  ntreq0  16741  adjeu  22394  dfiota3  23802  eqvinopb  24296  copsexgb  24297  dmoprabss6  24366  cmppar2  25304  pm11.58  26921  pm11.71  26928  2sbc5g  26949  iotasbc2  26953  stoweidlem60  27109  a9e2nd  27340  a9e2ndVD  27697  a9e2ndALT  27720  bnj1019  27823  bnj1209  27841  bnj1033  28011  bnj1189  28051
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