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

Theorem 19.41v 1854
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 1609 . 2  |-  F/ x ps
2119.41 1827 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1531
This theorem is referenced by:  19.41vv  1855  19.41vvv  1856  19.41vvvv  1857  eeeanv  1867  gencbvex  2843  euxfr  2964  euind  2965  zfpair  4228  opabn0  4311  eliunxp  4839  relop  4850  dmuni  4904  dmres  4992  dminss  5111  imainss  5112  ssrnres  5132  cnvresima  5178  resco  5193  rnco  5195  coass  5207  f11o  5522  rnoprab  5946  frxp  6241  omeu  6599  domen  6891  xpassen  6972  kmlem3  7794  cflem  7888  genpass  8649  ltexprlem4  8679  dftr6  24178  eeeeanv  25047  cnvresimaOLD  26329  prter2  26852  pm11.6  27694  pm11.71  27699  rfcnnnub  27810  3v3e3cycl2  28410  3v3e3cycl  28411  bnj534  29084  bnj906  29278  bnj908  29279  bnj916  29281  bnj983  29299  bnj986  29302  eeeanvOLD7  29658  dihglb2  32154
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