Theorem 19.41v 1901

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.xph /\ ps))

Distinct variable group:   ps,x

Allowed substitution hint:   ph(x)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/xps
2	1	19.41 1879	1 |- (E.x(ph /\ ps) <-> (E.xph /\ ps))

Syntax hints:   <-> wb 176   /\ wa 358  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  eeeanv  1914  gencbvex  2902  euxfr  3023  euind  3024  elpw11c  4148  elpw121c  4149  elpw131c  4150  elpw141c  4151  elpw151c  4152  elpw161c  4153  elpw171c  4154  elpw181c  4155  elpw191c  4156  elpw1101c  4157  elpw1111c  4158  eluni1g  4173  opkelcokg  4262  opkelimagekg  4272  dfimak2  4299  insklem  4305  ndisjrelk  4324  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  elsuc  4414  nnsucelrlem1  4425  ltfinex  4465  ssfin  4471  eqpwrelk  4479  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  srelk  4525  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  vfinspsslem1  4551  dfop2lem1  4574  opeq  4620  opabn0  4717  setconslem1  4732  setconslem2  4733  setconslem3  4734  setconslem7  4738  df1st2  4739  dfswap2  4742  eliunxp  4822  dmuni  4915  elimapw11c  4949  dmres  4987  rnuni  5039  dminss  5042  imainss  5043  ssrnres  5060  cnvresima  5078  resco  5086  rnco  5088  coass  5098  df2nd2  5112  f11o  5316  dmsi  5520  rnoprab  5577  brimage  5794  dmtxp  5803  txpcofun  5804  addcfnex  5825  brpprod  5840  dmpprod  5841  pw1fnf1o  5856  fundmen  6044  ceexlem1  6174  el2c  6192  taddc  6230  tcfnex  6245  csucex  6260  addccan2nclem1  6264  nchoicelem11  6300  nchoicelem16  6305