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

Theorem 19.41v 2034
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 1629 . 2  |-  F/ x ps
2119.41 1799 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   E.wex 1537
This theorem is referenced by:  19.41vv  2035  19.41vvv  2036  19.41vvvv  2037  eeeanv  2056  gencbvex  2768  euxfr  2888  euind  2889  zfpair  4106  opabn0  4188  eliunxp  4730  relop  4741  dmuni  4795  dmres  4883  dminss  5002  imainss  5003  ssrnres  5023  cnvresima  5068  resco  5083  rnco  5085  coass  5097  f11o  5363  rnoprab  5782  frxp  6077  omeu  6469  domen  6761  xpassen  6841  kmlem3  7662  cflem  7756  genpass  8513  ltexprlem4  8543  dftr6  23277  funpartfun  23655  eeeeanv  24109  cnvresimaOLD  25392  prter2  25915  pm11.6  26757  pm11.71  26762  bnj534  27457  bnj906  27651  bnj908  27652  bnj916  27654  bnj983  27672  bnj986  27675  dihglb2  30221
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator