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

Theorem 19.42v 2039
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 1800 1  |-  ( E. x ( ph  /\  ps )  <->  ( ph  /\  E. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537
This theorem is referenced by:  exdistr  2040  19.42vv  2041  19.42vvv  2042  4exdistr  2045  cbvex2  2049  2sb5  2075  2sb5rf  2080  rexcom4a  2776  ceqsex2  2792  reuind  2934  sbccomlem  3022  bm1.3ii  4104  eqvinop  4209  uniuni  4485  dmopabss  4864  dmopab3  4865  mptpreima  5139  fndmin  5552  zfrep6  5668  opabex3  5689  fliftf  5734  dfoprab2  5815  dmoprab  5848  dmoprabss  5849  fnoprabg  5865  fsplit  6143  eroveu  6707  rankuni  7489  aceq1  7698  dfac3  7702  kmlem14  7743  kmlem15  7744  axdc2lem  8028  1idpr  8607  ltexprlem1  8614  ltexprlem4  8617  shftdm  11517  ntreq0  16762  adjeu  22415  dfiota3  23823  eqvinopb  24317  copsexgb  24318  dmoprabss6  24387  cmppar2  25325  pm11.58  26942  pm11.71  26949  2sbc5g  26970  iotasbc2  26974  stoweidlem60  27130  a9e2nd  27361  a9e2ndVD  27718  a9e2ndALT  27741  bnj1019  27844  bnj1209  27862  bnj1033  28032  bnj1189  28072
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator