Theorem r19.42v 3170

Description: Restricted quantifier version of 19.42v 1955 (see also 19.42 2244). (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 3168	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3085	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  ceqsrexbv  3599  ceqsrex2v  3601  2reuswap  3693  2reuswap2  3694  2reu5  3705  2rmoswap  3708  dfiun2g  4973  iunrab  4996  iunin2  5014  iundif2  5017  reusv2lem4  5336  iunopab  5505  cnvuni  5833  elidinxp  6001  xpdifid  6124  dfpo2  6252  elunirn  7197  f1oiso  7297  oprabrexex2  7922  oeeu  8530  trcl  9638  dfac5lem2  10035  axgroth4  10744  rexuz2  12813  4fvwrd4  13565  divalglem10  16330  divalgb  16332  lsmelval2  21039  tgcmp  23344  hauscmplem  23349  unisngl  23470  xkobval  23529  txtube  23583  txcmplem1  23584  txkgen  23595  xkococnlem  23602  mbfaddlem  25605  mbfsup  25609  elaa  26264  dchrisumlem3  27442  elold  27839  colperpexlem3  28788  midex  28793  iscgra1  28866  ax5seg  28995  edglnl  29200  usgr2pth0  29822  hhcmpl  31260  sumdmdii  32475  reuxfrdf  32549  unipreima  32705  fpwrelmapffslem  32794  elirng  33836  esumfsup  34220  reprdifc  34777  bnj168  34879  bnj1398  35182  cvmliftlem15  35486  ellines  36340  bj-elsngl  37273  bj-dfmpoa  37428  ptrecube  37932  cnambfre  37980  islshpat  39454  lfl1dim  39558  glbconxN  39815  3dim0  39894  2dim  39907  1dimN  39908  islpln5  39972  islvol5  40016  dalem20  40130  lhpex2leN  40450  mapdval4N  42069  rexrabdioph  43225  rmxdioph  43447  expdiophlem1  43452  imaiun1  44081  coiun1  44082  ismnuprim  44724  prmunb2  44741  fourierdlem48  46586  2reuimp0  47548  2reuimp  47549  wtgoldbnnsum4prm  48236  bgoldbnnsum3prm  48238  dfvopnbgr2  48287  stgredgiun  48392  islindeps2  48917  isldepslvec2  48919  sepnsepolem1  49355