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

Theorem 19.42v 1928
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 1902 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550
This theorem is referenced by:  exdistr  1929  19.42vv  1930  19.42vvv  1931  4exdistr  1934  4exdistrOLD  1935  eeeanv  1938  cbvex2  1991  2sb5  2187  2sb5rf  2193  rexcom4a  2968  ceqsex2  2984  reuind  3129  2reu5lem3  3133  sbccomlem  3223  bm1.3ii  4325  eqvinop  4433  uniuni  4707  dmopabss  5072  dmopab3  5073  mptpreima  5354  brprcneu  5712  fndmin  5828  zfrep6  5959  opabex3d  5980  opabex3  5981  fliftf  6028  dfoprab2  6112  dmoprab  6145  dmoprabss  6146  fnoprabg  6162  fsplit  6442  eroveu  6990  rankuni  7778  aceq1  7987  dfac3  7991  kmlem14  8032  kmlem15  8033  axdc2lem  8317  1idpr  8895  ltexprlem1  8902  ltexprlem4  8905  shftdm  11874  ntreq0  17129  cnextf  18085  adjeu  23380  rexunirn  23966  mptfnf  24061  elfuns  25710  dfiota3  25718  brimg  25732  funpartlem  25737  itg2addnc  26205  pm11.58  27504  pm11.71  27511  2sbc5g  27531  iotasbc2  27535  stoweidlem60  27723  usg2spot2nb  28312  a9e2nd  28500  a9e2ndVD  28874  a9e2ndALT  28897  bnj1019  29004  bnj1209  29022  bnj1033  29192  bnj1189  29232  2sb5NEW7  29458  cbvex2OLD7  29570  2sb5rfOLD7  29600
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator