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

Theorem 19.42v 1846
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 1605 . 2  |-  F/ x ph
2119.42 1816 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528
This theorem is referenced by:  exdistr  1847  19.42vv  1848  19.42vvv  1849  4exdistr  1852  cbvex2  1945  2sb5  2051  2sb5rf  2056  rexcom4a  2808  ceqsex2  2824  reuind  2968  2reu5lem3  2972  sbccomlem  3061  bm1.3ii  4144  eqvinop  4251  uniuni  4527  dmopabss  4890  dmopab3  4891  mptpreima  5166  brprcneu  5518  fndmin  5632  zfrep6  5748  opabex3  5769  fliftf  5814  dfoprab2  5895  dmoprab  5928  dmoprabss  5929  fnoprabg  5945  fsplit  6223  eroveu  6753  rankuni  7535  aceq1  7744  dfac3  7748  kmlem14  7789  kmlem15  7790  axdc2lem  8074  1idpr  8653  ltexprlem1  8660  ltexprlem4  8663  shftdm  11566  ntreq0  16814  adjeu  22469  rexunirn  23140  mptfnf  23226  elfuns  24454  dfiota3  24462  eqvinopb  24965  copsexgb  24966  dmoprabss6  25035  cmppar2  25972  pm11.58  27589  pm11.71  27596  2sbc5g  27616  iotasbc2  27620  stoweidlem60  27809  a9e2nd  28324  a9e2ndVD  28684  a9e2ndALT  28707  bnj1019  28811  bnj1209  28829  bnj1033  28999  bnj1189  29039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator