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  3612  ceqsrex2v  3614  2reuswap  3706  2reuswap2  3707  2reu5  3718  2rmoswap  3721  dfiun2g  4987  iunrab  5010  iunin2  5028  iundif2  5031  reusv2lem4  5350  iunopab  5517  cnvuni  5845  elidinxp  6013  xpdifid  6136  dfpo2  6264  elunirn  7209  f1oiso  7309  oprabrexex2  7934  oeeu  8543  trcl  9651  dfac5lem2  10048  axgroth4  10757  rexuz2  12826  4fvwrd4  13578  divalglem10  16343  divalgb  16345  lsmelval2  21054  tgcmp  23362  hauscmplem  23367  unisngl  23488  xkobval  23547  txtube  23601  txcmplem1  23602  txkgen  23613  xkococnlem  23620  mbfaddlem  25634  mbfsup  25638  elaa  26297  dchrisumlem3  27475  elold  27872  colperpexlem3  28822  midex  28827  iscgra1  28900  ax5seg  29029  edglnl  29234  usgr2pth0  29856  hhcmpl  31294  sumdmdii  32509  reuxfrdf  32583  unipreima  32739  fpwrelmapffslem  32828  elirng  33870  esumfsup  34254  reprdifc  34811  bnj168  34913  bnj1398  35216  cvmliftlem15  35520  ellines  36374  bj-elsngl  37243  bj-dfmpoa  37398  ptrecube  37900  cnambfre  37948  islshpat  39422  lfl1dim  39526  glbconxN  39783  3dim0  39862  2dim  39875  1dimN  39876  islpln5  39940  islvol5  39984  dalem20  40098  lhpex2leN  40418  mapdval4N  42037  rexrabdioph  43180  rmxdioph  43402  expdiophlem1  43407  imaiun1  44036  coiun1  44037  ismnuprim  44679  prmunb2  44696  fourierdlem48  46541  2reuimp0  47503  2reuimp  47504  wtgoldbnnsum4prm  48191  bgoldbnnsum3prm  48193  dfvopnbgr2  48242  stgredgiun  48347  islindeps2  48872  isldepslvec2  48874  sepnsepolem1  49310