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

Theorem 19.41v 1920
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 1626 . 2  |-  F/ x ps
2119.41 1896 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547
This theorem is referenced by:  19.41vv  1921  19.41vvv  1922  19.41vvvv  1923  eeeanvOLD  1935  gencbvex  2958  euxfr  3080  euind  3081  zfpair  4361  opabn0  4445  eliunxp  4971  relop  4982  dmuni  5038  dmres  5126  dminss  5245  imainss  5246  ssrnres  5268  cnvresima  5318  resco  5333  rnco  5335  coass  5347  xpco  5373  f11o  5667  rnoprab  6115  frxp  6415  omeu  6787  domen  7080  xpassen  7161  kmlem3  7988  cflem  8082  genpass  8842  ltexprlem4  8872  hasheqf1oi  11590  3v3e3cycl2  21604  dftr6  25321  prter2  26620  pm11.6  27459  pm11.71  27464  rfcnnnub  27574  bnj534  28813  bnj906  29007  bnj908  29008  bnj916  29010  bnj983  29028  bnj986  29031  eeeanvOLD7  29388  dihglb2  31825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator