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

Theorem 19.42v 1929
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 1630 . 2  |-  F/ x ph
2119.42 1903 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551
This theorem is referenced by:  exdistr  1930  19.42vv  1931  19.42vvv  1932  4exdistr  1935  4exdistrOLD  1936  eeeanv  1939  cbvex2  1992  2sb5  2190  2sb5rf  2196  rexcom4a  2978  ceqsex2  2994  reuind  3139  2reu5lem3  3143  sbccomlem  3233  bm1.3ii  4336  eqvinop  4444  uniuni  4719  dmopabss  5084  dmopab3  5085  mptpreima  5366  brprcneu  5724  fndmin  5840  zfrep6  5971  opabex3d  5992  opabex3  5993  fliftf  6040  dfoprab2  6124  dmoprab  6157  dmoprabss  6158  fnoprabg  6174  fsplit  6454  eroveu  7002  rankuni  7792  aceq1  8003  dfac3  8007  kmlem14  8048  kmlem15  8049  axdc2lem  8333  1idpr  8911  ltexprlem1  8918  ltexprlem4  8921  shftdm  11891  ntreq0  17146  cnextf  18102  adjeu  23397  rexunirn  23983  mptfnf  24078  dfiota3  25773  brimg  25787  funpartlem  25792  itg2addnc  26273  pm11.58  27580  pm11.71  27587  2sbc5g  27607  iotasbc2  27611  stoweidlem60  27799  usg2spot2nb  28528  a9e2nd  28719  a9e2ndVD  29094  a9e2ndALT  29116  bnj1019  29224  bnj1209  29242  bnj1033  29412  bnj1189  29452  2sb5NEW7  29683  cbvex2OLD7  29805  2sb5rfOLD7  29835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator