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

Theorem 19.42v 1917
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 1626 . 2  |-  F/ x ph
2119.42 1891 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547
This theorem is referenced by:  exdistr  1918  19.42vv  1919  19.42vvv  1920  4exdistr  1923  4exdistrOLD  1924  eeeanv  1927  cbvex2  2039  2sb5  2145  2sb5rf  2151  rexcom4a  2919  ceqsex2  2935  reuind  3080  2reu5lem3  3084  sbccomlem  3174  bm1.3ii  4274  eqvinop  4382  uniuni  4656  dmopabss  5021  dmopab3  5022  mptpreima  5303  brprcneu  5661  fndmin  5776  zfrep6  5907  opabex3d  5928  opabex3  5929  fliftf  5976  dfoprab2  6060  dmoprab  6093  dmoprabss  6094  fnoprabg  6110  fsplit  6390  eroveu  6935  rankuni  7722  aceq1  7931  dfac3  7935  kmlem14  7976  kmlem15  7977  axdc2lem  8261  1idpr  8839  ltexprlem1  8846  ltexprlem4  8849  shftdm  11813  ntreq0  17064  cnextf  18018  adjeu  23240  rexunirn  23822  mptfnf  23915  elfuns  25478  dfiota3  25486  funpartlem  25505  itg2addnc  25959  pm11.58  27258  pm11.71  27265  2sbc5g  27285  iotasbc2  27289  stoweidlem60  27477  a9e2nd  27988  a9e2ndVD  28361  a9e2ndALT  28384  bnj1019  28488  bnj1209  28506  bnj1033  28676  bnj1189  28716  2sb5NEW7  28942  cbvex2OLD7  29047  2sb5rfOLD7  29078
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator