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

Theorem 19.41v 1853
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 1610 . 2  |-  F/ x ps
2119.41 1819 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1533
This theorem is referenced by:  19.41vv  1854  19.41vvv  1855  19.41vvvv  1856  eeeanv  1866  gencbvex  2831  euxfr  2952  euind  2953  zfpair  4211  opabn0  4294  eliunxp  4822  relop  4833  dmuni  4887  dmres  4975  dminss  5094  imainss  5095  ssrnres  5115  cnvresima  5160  resco  5175  rnco  5177  coass  5189  f11o  5471  rnoprab  5891  frxp  6186  omeu  6578  domen  6870  xpassen  6951  kmlem3  7773  cflem  7867  genpass  8628  ltexprlem4  8658  dftr6  23510  funpartfun  23888  eeeeanv  24342  cnvresimaOLD  25625  prter2  26148  pm11.6  26990  pm11.71  26995  rfcnnnub  27106  bnj534  28035  bnj906  28229  bnj908  28230  bnj916  28232  bnj983  28250  bnj986  28253  dihglb2  30799
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-11 1719
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1534  df-nf 1537
  Copyright terms: Public domain W3C validator