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

Theorem 19.41v 1925
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 1630 . 2  |-  F/ x ps
2119.41 1901 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1551
This theorem is referenced by:  19.41vv  1926  19.41vvv  1927  19.41vvvv  1928  eeeanvOLD  1940  gencbvex  3000  euxfr  3122  euind  3123  zfpair  4404  opabn0  4488  eliunxp  5015  relop  5026  dmuni  5082  dmres  5170  dminss  5289  imainss  5290  ssrnres  5312  cnvresima  5362  resco  5377  rnco  5379  coass  5391  xpco  5417  f11o  5711  rnoprab  6159  frxp  6459  omeu  6831  domen  7124  xpassen  7205  kmlem3  8037  cflem  8131  genpass  8891  ltexprlem4  8921  hasheqf1oi  11640  3v3e3cycl2  21656  dftr6  25378  prter2  26744  pm11.6  27582  pm11.71  27587  rfcnnnub  27697  bnj534  29181  bnj906  29375  bnj908  29376  bnj916  29378  bnj983  29396  bnj986  29399  eeeanvOLD7  29778  dihglb2  32214
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator