Theorem r19.42v 3196

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-rex 3089

This theorem is used by:  ceqsrexbv  3614  ceqsrex2v  3616  2reuswap  3708  2reuswap2  3709  2reu5  3720  2rmoswap  3723  dfiun2g  4993  iunrab  5016  iunin2  5034  iundif2  5037  reusv2lem4  5371  iunopab  5543  cnvuni  5875  elidinxp  6045  xpdifid  6164  xpdifcnvepel  6165  dfpo2  6297  elunirn  7249  f1oiso  7349  oprabrexex2  7973  oeeu  8587  trcl  9695  dfac5lem2  10115  axgroth4  10823  rexuz2  12929  4fvwrd4  13683  divalglem10  16466  divalgb  16468  lsmelval2  21217  tgcmp  23569  hauscmplem  23574  unisngl  23695  xkobval  23754  txtube  23808  txcmplem1  23809  txkgen  23820  xkococnlem  23827  mbfaddlem  25830  mbfsup  25834  elaa  26488  dchrisumlem3  27666  elold  28063  colperpexlem3  29024  midex  29029  iscgra1  29132  ax5seg  29299  edglnl  29504  usgr2pth0  30125  hhcmpl  31563  sumdmdii  32778  reuxfrdf  32848  unipreima  32999  fpwrelmapffslem  33088  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