Theorem r19.42v 3195

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  ceqsrexbv  3610  ceqsrex2v  3612  2reuswap  3704  2reuswap2  3705  2reu5  3716  2rmoswap  3719  dfiun2g  4988  iunrab  5011  iunin2  5029  iundif2  5032  reusv2lem4  5363  iunopab  5534  cnvuni  5868  elidinxp  6036  xpdifid  6159  xpdifcnvepel  6160  dfpo2  6299  elunirn  7255  f1oiso  7359  oprabrexex2  7990  oeeu  8612  trcl  9729  dfac5lem2  10203  axgroth4  10917  rexuz2  13026  4fvwrd4  13782  divalglem10  16572  divalgb  16574  lsmelval2  21360  tgcmp  23719  hauscmplem  23724  unisngl  23846  xkobval  23905  txtube  23959  txcmplem1  23960  txkgen  23971  xkococnlem  23978  mbfaddlem  25981  mbfsup  25985  elaa  26639  dchrisumlem3  27818  elold  28245  colperpexlem3  29208  midex  29213  iscgra1  29317  ax5seg  29516  edglnl  29721  usgr2pth0  30351  hhcmpl  31802  sumdmdii  33017  reuxfrdf  33087  unipreima  33237  fpwrelmapffslem  33324  elirng  34318  esumfsup  34702  reprdifc  35256  bnj168  35361  bnj1398  35664  cvmliftlem15  36063  ellines  36917  bj-elsngl  37881  bj-dfmpoa  38039  ptrecube  38538  cnambfre  38586  islshpat  40074  lfl1dim  40178  glbconxN  40435  3dim0  40514  2dim  40527  1dimN  40528  islpln5  40592  islvol5  40636  dalem20  40750  lhpex2leN  41070  mapdval4N  42689  rexrabdioph  43800  rmxdioph  44022  expdiophlem1  44027  imaiun1  44650  coiun1  44651  ismnuprim  45277  prmunb2  45294  fourierdlem48  47163  2reuimp0  48183  2reuimp  48184  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  dfvopnbgr2  48950  stgredgiun  49055  islindeps2  49594  isldepslvec2  49596  sepnsepolem1  50029