Theorem r19.42v 3194

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

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

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 3087

This theorem is used by:  ceqsrexbv  3610  ceqsrex2v  3612  2reuswap  3704  2reuswap2  3705  2reu5  3716  2rmoswap  3719  dfiun2g  4988  iunrab  5011  iunin2  5029  iundif2  5032  reusv2lem4  5366  iunopab  5538  cnvuni  5870  elidinxp  6040  xpdifid  6160  xpdifcnvepel  6161  dfpo2  6294  elunirn  7249  f1oiso  7353  oprabrexex2  7976  oeeu  8594  trcl  9710  dfac5lem2  10130  axgroth4  10844  rexuz2  12951  4fvwrd4  13706  divalglem10  16495  divalgb  16497  lsmelval2  21272  tgcmp  23629  hauscmplem  23634  unisngl  23756  xkobval  23815  txtube  23869  txcmplem1  23870  txkgen  23881  xkococnlem  23888  mbfaddlem  25891  mbfsup  25895  elaa  26551  dchrisumlem3  27730  elold  28127  colperpexlem3  29090  midex  29095  iscgra1  29199  ax5seg  29398  edglnl  29603  usgr2pth0  30233  hhcmpl  31684  sumdmdii  32899  reuxfrdf  32969  unipreima  33119  fpwrelmapffslem  33206  elirng  34199  esumfsup  34583  reprdifc  35138  bnj168  35243  bnj1398  35546  cvmliftlem15  35880  ellines  36735  bj-elsngl  37715  bj-dfmpoa  37871  ptrecube  38372  cnambfre  38420  islshpat  39893  lfl1dim  39997  glbconxN  40254  3dim0  40333  2dim  40346  1dimN  40347  islpln5  40411  islvol5  40455  dalem20  40569  lhpex2leN  40889  mapdval4N  42508  rexrabdioph  43638  rmxdioph  43860  expdiophlem1  43865  imaiun1  44494  coiun1  44495  ismnuprim  45121  prmunb2  45138  fourierdlem48  46985  2reuimp0  48005  2reuimp  48006  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  dfvopnbgr2  48772  stgredgiun  48877  islindeps2  49416  isldepslvec2  49418  sepnsepolem1  49851