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

Theorem 19.42v 1858
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 1609 . 2  |-  F/ x ph
2119.42 1828 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531
This theorem is referenced by:  exdistr  1859  19.42vv  1860  19.42vvv  1861  4exdistr  1864  cbvex2  1958  2sb5  2064  2sb5rf  2069  rexcom4a  2821  ceqsex2  2837  reuind  2981  2reu5lem3  2985  sbccomlem  3074  bm1.3ii  4160  eqvinop  4267  uniuni  4543  dmopabss  4906  dmopab3  4907  mptpreima  5182  brprcneu  5534  fndmin  5648  zfrep6  5764  opabex3  5785  fliftf  5830  dfoprab2  5911  dmoprab  5944  dmoprabss  5945  fnoprabg  5961  fsplit  6239  eroveu  6769  rankuni  7551  aceq1  7760  dfac3  7764  kmlem14  7805  kmlem15  7806  axdc2lem  8090  1idpr  8669  ltexprlem1  8676  ltexprlem4  8679  shftdm  11582  ntreq0  16830  adjeu  22485  rexunirn  23156  mptfnf  23241  elfuns  24525  dfiota3  24533  funpartlem  24552  itg2addnc  25005  eqvinopb  25068  copsexgb  25069  dmoprabss6  25138  cmppar2  26075  pm11.58  27692  pm11.71  27699  2sbc5g  27719  iotasbc2  27723  stoweidlem60  27912  opabex3d  28190  a9e2nd  28623  a9e2ndVD  29000  a9e2ndALT  29023  bnj1019  29127  bnj1209  29145  bnj1033  29315  bnj1189  29355  2sb5NEW7  29581  cbvex2OLD7  29685  2sb5rfOLD7  29717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator