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

Theorem 19.41v 2035
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  2036  19.41vvv  2037  19.41vvvv  2038  eeeanv  2059  gencbvex  2805  euxfr  2926  euind  2927  zfpair  4184  opabn0  4267  eliunxp  4811  relop  4822  dmuni  4876  dmres  4964  dminss  5083  imainss  5084  ssrnres  5104  cnvresima  5149  resco  5164  rnco  5166  coass  5178  f11o  5444  rnoprab  5864  frxp  6159  omeu  6551  domen  6843  xpassen  6924  kmlem3  7746  cflem  7840  genpass  8601  ltexprlem4  8631  dftr6  23478  funpartfun  23856  eeeeanv  24310  cnvresimaOLD  25593  prter2  26116  pm11.6  26958  pm11.71  26963  rfcnnnub  27075  bnj534  27817  bnj906  28011  bnj908  28012  bnj916  28014  bnj983  28032  bnj986  28035  dihglb2  30699
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