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  4403  opabn0  4487  eliunxp  5014  relop  5025  dmuni  5081  dmres  5169  dminss  5288  imainss  5289  ssrnres  5311  cnvresima  5361  resco  5376  rnco  5378  coass  5390  xpco  5416  f11o  5710  rnoprab  6158  frxp  6458  omeu  6830  domen  7123  xpassen  7204  kmlem3  8034  cflem  8128  genpass  8888  ltexprlem4  8918  hasheqf1oi  11637  3v3e3cycl2  21653  dftr6  25375  prter2  26732  pm11.6  27570  pm11.71  27575  rfcnnnub  27685  bnj534  29169  bnj906  29363  bnj908  29364  bnj916  29366  bnj983  29384  bnj986  29387  eeeanvOLD7  29766  dihglb2  32202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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