Theorem r19.42v 3170

Description: Restricted quantifier version of 19.42v 1955 (see also 19.42 2244). (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 3168	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3085	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  ceqsrexbv  3612  ceqsrex2v  3614  2reuswap  3706  2reuswap2  3707  2reu5  3718  2rmoswap  3721  dfiun2g  4987  iunrab  5010  iunin2  5028  iundif2  5031  reusv2lem4  5348  iunopab  5515  cnvuni  5843  elidinxp  6011  xpdifid  6134  dfpo2  6262  elunirn  7207  f1oiso  7307  oprabrexex2  7932  oeeu  8541  trcl  9649  dfac5lem2  10046  axgroth4  10755  rexuz2  12824  4fvwrd4  13576  divalglem10  16341  divalgb  16343  lsmelval2  21052  tgcmp  23360  hauscmplem  23365  unisngl  23486  xkobval  23545  txtube  23599  txcmplem1  23600  txkgen  23611  xkococnlem  23618  mbfaddlem  25632  mbfsup  25636  elaa  26295  dchrisumlem3  27473  elold  27870  colperpexlem3  28820  midex  28825  iscgra1  28898  ax5seg  29027  edglnl  29232  usgr2pth0  29854  hhcmpl  31292  sumdmdii  32507  reuxfrdf  32581  unipreima  32737  fpwrelmapffslem  32826  elirng  33868  esumfsup  34252  reprdifc  34809  bnj168  34911  bnj1398  35214  cvmliftlem15  35518  ellines  36372  bj-elsngl  37220  bj-dfmpoa  37375  ptrecube  37875  cnambfre  37923  islshpat  39397  lfl1dim  39501  glbconxN  39758  3dim0  39837  2dim  39850  1dimN  39851  islpln5  39915  islvol5  39959  dalem20  40073  lhpex2leN  40393  mapdval4N  42012  rexrabdioph  43155  rmxdioph  43377  expdiophlem1  43382  imaiun1  44011  coiun1  44012  ismnuprim  44654  prmunb2  44671  fourierdlem48  46516  2reuimp0  47478  2reuimp  47479  wtgoldbnnsum4prm  48166  bgoldbnnsum3prm  48168  dfvopnbgr2  48217  stgredgiun  48322  islindeps2  48847  isldepslvec2  48849  sepnsepolem1  49285