Theorem r19.42v 3253

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

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-rex 3057

This theorem is referenced by:  rexcom  3258  ceqsrexbv  3554  ceqsrex2v  3555  2reuswap  3648  2reuswap2  3649  2reu5  3660  2rmoswap  3663  iunrab  4947  iunin2  4965  iundif2  4968  reusv2lem4  5279  iunopab  5425  cnvuni  5740  elidinxp  5896  xpdifid  6011  elunirn  7042  f1oiso  7138  oprabrexex2  7729  oeeu  8309  trcl  9322  dfac5lem2  9703  axgroth4  10411  rexuz2  12460  4fvwrd4  13197  cshwsexa  14354  divalglem10  15926  divalgb  15928  lsmelval2  20076  tgcmp  22252  hauscmplem  22257  unisngl  22378  xkobval  22437  txtube  22491  txcmplem1  22492  txkgen  22503  xkococnlem  22510  mbfaddlem  24511  mbfsup  24515  elaa  25163  dchrisumlem3  26326  colperpexlem3  26777  midex  26782  iscgra1  26855  ax5seg  26983  edglnl  27188  usgr2pth0  27806  hhcmpl  29235  sumdmdii  30450  reuxfrdf  30512  unipreima  30654  fpwrelmapffslem  30741  esumfsup  31704  reprdifc  32273  bnj168  32375  bnj1398  32681  cvmliftlem15  32927  dfpo2  33392  elold  33739  ellines  34140  bj-elsngl  34844  bj-dfmpoa  34973  ptrecube  35463  cnambfre  35511  islshpat  36717  lfl1dim  36821  glbconxN  37078  3dim0  37157  2dim  37170  1dimN  37171  islpln5  37235  islvol5  37279  dalem20  37393  lhpex2leN  37713  mapdval4N  39332  rexrabdioph  40260  rmxdioph  40482  expdiophlem1  40487  imaiun1  40877  coiun1  40878  ismnuprim  41526  prmunb2  41543  fourierdlem48  43313  2reuimp0  44221  2reuimp  44222  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  islindeps2  45440  isldepslvec2  45442  sepnsepolem1  45831