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  5340  iunopab  5509  cnvuni  5837  elidinxp  6005  xpdifid  6128  dfpo2  6256  elunirn  7201  f1oiso  7301  oprabrexex2  7926  oeeu  8534  trcl  9644  dfac5lem2  10041  axgroth4  10750  rexuz2  12844  4fvwrd4  13597  divalglem10  16366  divalgb  16368  lsmelval2  21076  tgcmp  23380  hauscmplem  23385  unisngl  23506  xkobval  23565  txtube  23619  txcmplem1  23620  txkgen  23631  xkococnlem  23638  mbfaddlem  25641  mbfsup  25645  elaa  26297  dchrisumlem3  27472  elold  27869  colperpexlem3  28818  midex  28823  iscgra1  28896  ax5seg  29025  edglnl  29230  usgr2pth0  29852  hhcmpl  31290  sumdmdii  32505  reuxfrdf  32579  unipreima  32735  fpwrelmapffslem  32824  elirng  33850  esumfsup  34234  reprdifc  34791  bnj168  34893  bnj1398  35196  cvmliftlem15  35500  ellines  36354  bj-elsngl  37295  bj-dfmpoa  37450  ptrecube  37959  cnambfre  38007  islshpat  39481  lfl1dim  39585  glbconxN  39842  3dim0  39921  2dim  39934  1dimN  39935  islpln5  39999  islvol5  40043  dalem20  40157  lhpex2leN  40477  mapdval4N  42096  rexrabdioph  43244  rmxdioph  43466  expdiophlem1  43471  imaiun1  44100  coiun1  44101  ismnuprim  44743  prmunb2  44760  fourierdlem48  46604  2reuimp0  47578  2reuimp  47579  wtgoldbnnsum4prm  48294  bgoldbnnsum3prm  48296  dfvopnbgr2  48345  stgredgiun  48450  islindeps2  48975  isldepslvec2  48977  sepnsepolem1  49413