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

Theorem 19.41v 1842
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 1605 . 2  |-  F/ x ps
2119.41 1815 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528
This theorem is referenced by:  19.41vv  1843  19.41vvv  1844  19.41vvvv  1845  eeeanv  1855  gencbvex  2830  euxfr  2951  euind  2952  zfpair  4212  opabn0  4295  eliunxp  4823  relop  4834  dmuni  4888  dmres  4976  dminss  5095  imainss  5096  ssrnres  5116  cnvresima  5162  resco  5177  rnco  5179  coass  5191  f11o  5506  rnoprab  5930  frxp  6225  omeu  6583  domen  6875  xpassen  6956  kmlem3  7778  cflem  7872  genpass  8633  ltexprlem4  8663  dftr6  24107  funpartfun  24481  eeeeanv  24944  cnvresimaOLD  26226  prter2  26749  pm11.6  27591  pm11.71  27596  rfcnnnub  27707  bnj534  28768  bnj906  28962  bnj908  28963  bnj916  28965  bnj983  28983  bnj986  28986  dihglb2  31532
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