Theorem r19.42v 3278

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

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-rex 3071

This theorem is referenced by:  rexcom  3283  ceqsrexbv  3587  ceqsrex2v  3588  2reuswap  3684  2reuswap2  3685  2reu5  3696  2rmoswap  3699  iunrab  4986  iunin2  5004  iundif2  5007  reusv2lem4  5327  iunopab  5473  cnvuni  5792  elidinxp  5948  xpdifid  6068  dfpo2  6196  elunirn  7118  f1oiso  7215  oprabrexex2  7807  oeeu  8410  trcl  9469  dfac5lem2  9864  axgroth4  10572  rexuz2  12621  4fvwrd4  13358  cshwsexa  14518  divalglem10  16092  divalgb  16094  lsmelval2  20328  tgcmp  22533  hauscmplem  22538  unisngl  22659  xkobval  22718  txtube  22772  txcmplem1  22773  txkgen  22784  xkococnlem  22791  mbfaddlem  24805  mbfsup  24809  elaa  25457  dchrisumlem3  26620  colperpexlem3  27074  midex  27079  iscgra1  27152  ax5seg  27287  edglnl  27494  usgr2pth0  28112  hhcmpl  29541  sumdmdii  30756  reuxfrdf  30818  unipreima  30960  fpwrelmapffslem  31046  esumfsup  32017  reprdifc  32586  bnj168  32688  bnj1398  32993  cvmliftlem15  33239  elold  34032  ellines  34433  bj-elsngl  35137  bj-dfmpoa  35268  ptrecube  35756  cnambfre  35804  islshpat  37010  lfl1dim  37114  glbconxN  37371  3dim0  37450  2dim  37463  1dimN  37464  islpln5  37528  islvol5  37572  dalem20  37686  lhpex2leN  38006  mapdval4N  39625  rexrabdioph  40596  rmxdioph  40818  expdiophlem1  40823  imaiun1  41212  coiun1  41213  ismnuprim  41865  prmunb2  41882  fourierdlem48  43649  2reuimp0  44557  2reuimp  44558  wtgoldbnnsum4prm  45206  bgoldbnnsum3prm  45208  islindeps2  45776  isldepslvec2  45778  sepnsepolem1  46167