Theorem r19.42v 3195

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

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-rex 3088

This theorem is referenced by:  ceqsrexbv  3616  ceqsrex2v  3618  2reuswap  3710  2reuswap2  3711  2reu5  3722  2rmoswap  3725  dfiun2g  4988  iunrab  5011  iunin2  5029  iundif2  5032  reusv2lem4  5359  iunopab  5531  cnvuni  5863  elidinxp  6034  xpdifid  6154  xpdifcnvepel  6155  dfpo2  6284  elunirn  7236  f1oiso  7336  oprabrexex2  7960  oeeu  8574  trcl  9684  dfac5lem2  10081  axgroth4  10791  rexuz2  12901  4fvwrd4  13654  divalglem10  16437  divalgb  16439  lsmelval2  21153  tgcmp  23462  hauscmplem  23467  unisngl  23588  xkobval  23647  txtube  23701  txcmplem1  23702  txkgen  23713  xkococnlem  23720  mbfaddlem  25723  mbfsup  25727  elaa  26381  dchrisumlem3  27556  elold  27953  colperpexlem3  28906  midex  28911  iscgra1  29005  ax5seg  29140  edglnl  29345  usgr2pth0  29966  hhcmpl  31404  sumdmdii  32619  reuxfrdf  32691  unipreima  32846  fpwrelmapffslem  32935  elirng  33984  esumfsup  34368  reprdifc  34922  bnj168  35027  bnj1398  35330  cvmliftlem15  35649  ellines  36503  bj-elsngl  37454  bj-dfmpoa  37609  ptrecube  38120  cnambfre  38168  islshpat  39642  lfl1dim  39746  glbconxN  40003  3dim0  40082  2dim  40095  1dimN  40096  islpln5  40160  islvol5  40204  dalem20  40318  lhpex2leN  40638  mapdval4N  42257  rexrabdioph  43372  rmxdioph  43594  expdiophlem1  43599  imaiun1  44228  coiun1  44229  ismnuprim  44871  prmunb2  44888  fourierdlem48  46729  2reuimp0  47709  2reuimp  47710  wtgoldbnnsum4prm  48425  bgoldbnnsum3prm  48427  dfvopnbgr2  48476  stgredgiun  48581  islindeps2  49106  isldepslvec2  49108  sepnsepolem1  49544