Theorem r19.42v 3164

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  ceqsrexbv  3606  ceqsrex2v  3608  2reuswap  3700  2reuswap2  3701  2reu5  3712  2rmoswap  3715  dfiun2g  4978  iunrab  4999  iunin2  5017  iundif2  5020  reusv2lem4  5337  iunopab  5497  cnvuni  5825  elidinxp  5992  xpdifid  6115  dfpo2  6243  elunirn  7185  f1oiso  7285  oprabrexex2  7910  oeeu  8518  trcl  9618  dfac5lem2  10015  axgroth4  10723  rexuz2  12797  4fvwrd4  13548  divalglem10  16313  divalgb  16315  lsmelval2  21019  tgcmp  23316  hauscmplem  23321  unisngl  23442  xkobval  23501  txtube  23555  txcmplem1  23556  txkgen  23567  xkococnlem  23574  mbfaddlem  25588  mbfsup  25592  elaa  26251  dchrisumlem3  27429  elold  27814  0reno  28399  colperpexlem3  28710  midex  28715  iscgra1  28788  ax5seg  28916  edglnl  29121  usgr2pth0  29743  hhcmpl  31180  sumdmdii  32395  reuxfrdf  32470  unipreima  32625  fpwrelmapffslem  32715  elirng  33699  esumfsup  34083  reprdifc  34640  bnj168  34742  bnj1398  35046  cvmliftlem15  35342  ellines  36196  bj-elsngl  37012  bj-dfmpoa  37162  ptrecube  37670  cnambfre  37718  islshpat  39126  lfl1dim  39230  glbconxN  39487  3dim0  39566  2dim  39579  1dimN  39580  islpln5  39644  islvol5  39688  dalem20  39802  lhpex2leN  40122  mapdval4N  41741  rexrabdioph  42897  rmxdioph  43119  expdiophlem1  43124  imaiun1  43754  coiun1  43755  ismnuprim  44397  prmunb2  44414  fourierdlem48  46262  2reuimp0  47224  2reuimp  47225  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  dfvopnbgr2  47963  stgredgiun  48068  islindeps2  48594  isldepslvec2  48596  sepnsepolem1  49032