Theorem r19.42v 3191

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexcomOLD  3291  ceqsrexbv  3656  ceqsrex2v  3658  2reuswap  3752  2reuswap2  3753  2reu5  3764  2rmoswap  3767  dfiun2g  5030  iunrab  5052  iunin2  5071  iundif2  5074  reusv2lem4  5401  iunopab  5564  iunopabOLD  5565  cnvuni  5897  elidinxp  6062  xpdifid  6188  dfpo2  6316  elunirn  7271  f1oiso  7371  oprabrexex2  8003  oeeu  8641  trcl  9768  dfac5lem2  10164  axgroth4  10872  rexuz2  12941  4fvwrd4  13688  cshwsexaOLD  14863  divalglem10  16439  divalgb  16441  lsmelval2  21084  tgcmp  23409  hauscmplem  23414  unisngl  23535  xkobval  23594  txtube  23648  txcmplem1  23649  txkgen  23660  xkococnlem  23667  mbfaddlem  25695  mbfsup  25699  elaa  26358  dchrisumlem3  27535  elold  27908  0reno  28429  colperpexlem3  28740  midex  28745  iscgra1  28818  ax5seg  28953  edglnl  29160  usgr2pth0  29785  hhcmpl  31219  sumdmdii  32434  reuxfrdf  32510  unipreima  32653  fpwrelmapffslem  32743  elirng  33736  esumfsup  34071  reprdifc  34642  bnj168  34744  bnj1398  35048  cvmliftlem15  35303  ellines  36153  bj-elsngl  36969  bj-dfmpoa  37119  ptrecube  37627  cnambfre  37675  islshpat  39018  lfl1dim  39122  glbconxN  39380  3dim0  39459  2dim  39472  1dimN  39473  islpln5  39537  islvol5  39581  dalem20  39695  lhpex2leN  40015  mapdval4N  41634  rexrabdioph  42805  rmxdioph  43028  expdiophlem1  43033  imaiun1  43664  coiun1  43665  ismnuprim  44313  prmunb2  44330  fourierdlem48  46169  2reuimp0  47126  2reuimp  47127  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  dfvopnbgr2  47839  stgredgiun  47925  islindeps2  48400  isldepslvec2  48402  sepnsepolem1  48819