Theorem r19.42v 3199

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

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

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 3092

This theorem is used by:  ceqsrexbv  3617  ceqsrex2v  3619  2reuswap  3711  2reuswap2  3712  2reu5  3723  2rmoswap  3726  dfiun2g  4996  iunrab  5019  iunin2  5037  iundif2  5040  reusv2lem4  5374  iunopab  5546  cnvuni  5878  elidinxp  6048  xpdifid  6167  xpdifcnvepel  6168  dfpo2  6301  elunirn  7254  f1oiso  7358  oprabrexex2  7981  oeeu  8595  trcl  9704  dfac5lem2  10124  axgroth4  10836  rexuz2  12943  4fvwrd4  13697  divalglem10  16486  divalgb  16488  lsmelval2  21260  tgcmp  23612  hauscmplem  23617  unisngl  23739  xkobval  23798  txtube  23852  txcmplem1  23853  txkgen  23864  xkococnlem  23871  mbfaddlem  25874  mbfsup  25878  elaa  26532  dchrisumlem3  27710  elold  28107  colperpexlem3  29068  midex  29073  iscgra1  29176  ax5seg  29347  edglnl  29552  usgr2pth0  30182  hhcmpl  31627  sumdmdii  32842  reuxfrdf  32912  unipreima  33063  fpwrelmapffslem  33151  elirng  34144  esumfsup  34528  reprdifc  35083  bnj168  35188  bnj1398  35491  cvmliftlem15  35831  ellines  36685  bj-elsngl  37665  bj-dfmpoa  37821  ptrecube  38332  cnambfre  38380  islshpat  39853  lfl1dim  39957  glbconxN  40214  3dim0  40293  2dim  40306  1dimN  40307  islpln5  40371  islvol5  40415  dalem20  40529  lhpex2leN  40849  mapdval4N  42468  rexrabdioph  43598  rmxdioph  43820  expdiophlem1  43825  imaiun1  44454  coiun1  44455  ismnuprim  45081  prmunb2  45098  fourierdlem48  46945  2reuimp0  47928  2reuimp  47929  wtgoldbnnsum4prm  48644  bgoldbnnsum3prm  48646  dfvopnbgr2  48695  stgredgiun  48800  islindeps2  49339  isldepslvec2  49341  sepnsepolem1  49776