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

Theorem 19.41v 1932
Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 21-Jun-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 1674 . 2  |-  F/ x ps
2119.41 1911 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  19.41vv  1933  19.41vvv  1934  19.41vvvv  1935  gencbvex  3122  euxfr  3252  euind  3253  zfpair  4638  opabn0  4728  eliunxp  5086  relop  5099  dmuni  5158  dmres  5240  dminss  5360  imainss  5361  ssrnres  5385  cnvresima  5436  resco  5451  rnco  5453  coass  5465  xpco  5486  rnoprab  6284  f11o  6650  frxp  6793  omeu  7135  domen  7434  xpassen  7516  kmlem3  8433  cflem  8527  genpass  9290  ltexprlem4  9320  hasheqf1oi  12240  3v3e3cycl2  23703  dftr6  27705  prter2  29175  pm11.6  29794  pm11.71  29799  rfcnnnub  29907  eliunxp2  30870  bnj534  32064  bnj906  32256  bnj908  32257  bnj916  32259  bnj983  32277  bnj986  32280  bj-eeanvw  32536  bj-csbsnlem  32738  bj-ccinftydisj  32875  dihglb2  35326
  Copyright terms: Public domain W3C validator