Theorem r19.42v 3280

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  rexcomOLD  3286  ceqsrexbv  3587  ceqsrex2v  3588  2reuswap  3682  2reuswap2  3683  2reu5  3694  2rmoswap  3697  dfiun2g  4961  iunrab  4983  iunin2  5001  iundif2  5004  reusv2lem4  5325  iunopab  5473  iunopabOLD  5474  cnvuni  5798  elidinxp  5954  xpdifid  6076  dfpo2  6203  elunirn  7133  f1oiso  7231  oprabrexex2  7830  oeeu  8443  trcl  9495  dfac5lem2  9889  axgroth4  10597  rexuz2  12648  4fvwrd4  13385  cshwsexa  14546  divalglem10  16120  divalgb  16122  lsmelval2  20356  tgcmp  22561  hauscmplem  22566  unisngl  22687  xkobval  22746  txtube  22800  txcmplem1  22801  txkgen  22812  xkococnlem  22819  mbfaddlem  24833  mbfsup  24837  elaa  25485  dchrisumlem3  26648  colperpexlem3  27102  midex  27107  iscgra1  27180  ax5seg  27315  edglnl  27522  usgr2pth0  28142  hhcmpl  29571  sumdmdii  30786  reuxfrdf  30848  unipreima  30990  fpwrelmapffslem  31076  esumfsup  32047  reprdifc  32616  bnj168  32718  bnj1398  33023  cvmliftlem15  33269  elold  34062  ellines  34463  bj-elsngl  35167  bj-dfmpoa  35298  ptrecube  35786  cnambfre  35834  islshpat  37038  lfl1dim  37142  glbconxN  37399  3dim0  37478  2dim  37491  1dimN  37492  islpln5  37556  islvol5  37600  dalem20  37714  lhpex2leN  38034  mapdval4N  39653  rexrabdioph  40623  rmxdioph  40845  expdiophlem1  40850  imaiun1  41266  coiun1  41267  ismnuprim  41919  prmunb2  41936  fourierdlem48  43702  2reuimp0  44617  2reuimp  44618  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  islindeps2  45835  isldepslvec2  45837  sepnsepolem1  46226