Theorem r19.42v 3168

Description: Restricted quantifier version of 19.42v 1954 (see also 19.42 2243). (Contributed by NM, 27-May-1998.)

Assertion

Ref	Expression
r19.42v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.42v

Step	Hyp	Ref	Expression
1		r19.41v 3166	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3083	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  ceqsrexbv  3610  ceqsrex2v  3612  2reuswap  3704  2reuswap2  3705  2reu5  3716  2rmoswap  3719  dfiun2g  4985  iunrab  5008  iunin2  5026  iundif2  5029  reusv2lem4  5346  iunopab  5507  cnvuni  5835  elidinxp  6003  xpdifid  6126  dfpo2  6254  elunirn  7197  f1oiso  7297  oprabrexex2  7922  oeeu  8531  trcl  9639  dfac5lem2  10036  axgroth4  10745  rexuz2  12814  4fvwrd4  13566  divalglem10  16331  divalgb  16333  lsmelval2  21039  tgcmp  23347  hauscmplem  23352  unisngl  23473  xkobval  23532  txtube  23586  txcmplem1  23587  txkgen  23598  xkococnlem  23605  mbfaddlem  25619  mbfsup  25623  elaa  26282  dchrisumlem3  27460  elold  27857  colperpexlem3  28806  midex  28811  iscgra1  28884  ax5seg  29013  edglnl  29218  usgr2pth0  29840  hhcmpl  31277  sumdmdii  32492  reuxfrdf  32567  unipreima  32723  fpwrelmapffslem  32813  elirng  33845  esumfsup  34229  reprdifc  34786  bnj168  34888  bnj1398  35192  cvmliftlem15  35494  ellines  36348  bj-elsngl  37171  bj-dfmpoa  37325  ptrecube  37823  cnambfre  37871  islshpat  39299  lfl1dim  39403  glbconxN  39660  3dim0  39739  2dim  39752  1dimN  39753  islpln5  39817  islvol5  39861  dalem20  39975  lhpex2leN  40295  mapdval4N  41914  rexrabdioph  43057  rmxdioph  43279  expdiophlem1  43284  imaiun1  43913  coiun1  43914  ismnuprim  44556  prmunb2  44573  fourierdlem48  46419  2reuimp0  47381  2reuimp  47382  wtgoldbnnsum4prm  48069  bgoldbnnsum3prm  48071  dfvopnbgr2  48120  stgredgiun  48225  islindeps2  48750  isldepslvec2  48752  sepnsepolem1  49188