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

Theorem 19.41v 1938
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 1678 . 2  |-  F/ x ps
2119.41 1915 1  |-  ( E. x ( ph  /\  ps )  <->  ( E. x ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595
This theorem is referenced by:  19.41vv  1939  19.41vvv  1940  19.41vvvv  1941  gencbvex  3150  euxfr  3282  euind  3283  zfpair  4677  opabn0  4771  eliunxp  5131  relop  5144  dmuni  5203  dmres  5285  dminss  5411  imainss  5412  ssrnres  5436  cnvresima  5487  resco  5502  rnco  5504  coass  5517  xpco  5538  rnoprab  6360  f11o  6736  frxp  6883  omeu  7224  domen  7519  xpassen  7601  kmlem3  8521  cflem  8615  genpass  9376  ltexprlem4  9406  hasheqf1oi  12379  3v3e3cycl2  24326  dftr6  28742  prter2  30213  pm11.6  30831  pm11.71  30836  rfcnnnub  30944  eliunxp2  31862  bnj534  32750  bnj906  32942  bnj908  32943  bnj916  32945  bnj983  32963  bnj986  32966  bj-eeanvw  33224  bj-csbsnlem  33426  bj-ccinftydisj  33563  dihglb2  36014
  Copyright terms: Public domain W3C validator