Theorem r19.42v 3197

Description: Restricted quantifier version of 19.42v 1983 (see also 19.42 2272). (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 3195	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 465	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3112	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 465	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is used by:  ceqsrexbv  3615  ceqsrex2v  3617  2reuswap  3709  2reuswap2  3710  2reu5  3721  2rmoswap  3724  dfiun2g  4994  iunrab  5017  iunin2  5035  iundif2  5038  reusv2lem4  5372  iunopab  5544  cnvuni  5876  elidinxp  6046  xpdifid  6165  xpdifcnvepel  6166  dfpo2  6297  elunirn  7249  f1oiso  7349  oprabrexex2  7971  oeeu  8585  trcl  9693  dfac5lem2  10113  axgroth4  10821  rexuz2  12927  4fvwrd4  13681  divalglem10  16464  divalgb  16466  lsmelval2  21215  tgcmp  23567  hauscmplem  23572  unisngl  23693  xkobval  23752  txtube  23806  txcmplem1  23807  txkgen  23818  xkococnlem  23825  mbfaddlem  25828  mbfsup  25832  elaa  26486  dchrisumlem3  27664  elold  28061  colperpexlem3  29022  midex  29027  iscgra1  29130  ax5seg  29297  edglnl  29502  usgr2pth0  30123  hhcmpl  31561  sumdmdii  32776  reuxfrdf  32846  unipreima  32997  fpwrelmapffslem  33086  elirng  34085  esumfsup  34469  reprdifc  35023  bnj168  35128  bnj1398  35431  cvmliftlem15  35798  ellines  36652  bj-elsngl  37632  bj-dfmpoa  37788  ptrecube  38299  cnambfre  38347  islshpat  39819  lfl1dim  39923  glbconxN  40180  3dim0  40259  2dim  40272  1dimN  40273  islpln5  40337  islvol5  40381  dalem20  40495  lhpex2leN  40815  mapdval4N  42434  rexrabdioph  43549  rmxdioph  43771  expdiophlem1  43776  imaiun1  44405  coiun1  44406  ismnuprim  45032  prmunb2  45049  fourierdlem48  46896  2reuimp0  47879  2reuimp  47880  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  dfvopnbgr2  48646  stgredgiun  48751  islindeps2  49291  isldepslvec2  49293  sepnsepolem1  49728