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

Theorem 19.41v 2035
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.41v  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem 19.41v
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ps
2119.41 1799 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537
This theorem is referenced by:  19.41vv  2036  19.41vvv  2037  19.41vvvv  2038  eeeanv  2059  gencbvex  2781  euxfr  2902  euind  2903  zfpair  4150  opabn0  4232  eliunxp  4776  relop  4787  dmuni  4841  dmres  4929  dminss  5048  imainss  5049  ssrnres  5069  cnvresima  5114  resco  5129  rnco  5131  coass  5143  f11o  5409  rnoprab  5829  frxp  6124  omeu  6516  domen  6808  xpassen  6889  kmlem3  7711  cflem  7805  genpass  8566  ltexprlem4  8596  dftr6  23443  funpartfun  23821  eeeeanv  24275  cnvresimaOLD  25558  prter2  26081  pm11.6  26923  pm11.71  26928  rfcnnnub  27040  bnj534  27780  bnj906  27974  bnj908  27975  bnj916  27977  bnj983  27995  bnj986  27998  dihglb2  30662
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