Theorem r19.42v 3188

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wrex 3068

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  rexcomOLD  3286  ceqsrexbv  3643  ceqsrex2v  3645  2reuswap  3741  2reuswap2  3742  2reu5  3753  2rmoswap  3756  dfiun2g  5032  iunrab  5054  iunin2  5073  iundif2  5076  reusv2lem4  5398  iunopab  5558  iunopabOLD  5559  cnvuni  5885  elidinxp  6042  xpdifid  6166  dfpo2  6294  elunirn  7252  f1oiso  7350  oprabrexex2  7967  oeeu  8605  trcl  9725  dfac5lem2  10121  axgroth4  10829  rexuz2  12887  4fvwrd4  13625  cshwsexaOLD  14779  divalglem10  16349  divalgb  16351  lsmelval2  20840  tgcmp  23125  hauscmplem  23130  unisngl  23251  xkobval  23310  txtube  23364  txcmplem1  23365  txkgen  23376  xkococnlem  23383  mbfaddlem  25409  mbfsup  25413  elaa  26065  dchrisumlem3  27230  elold  27601  colperpexlem3  28250  midex  28255  iscgra1  28328  ax5seg  28463  edglnl  28670  usgr2pth0  29289  hhcmpl  30720  sumdmdii  31935  reuxfrdf  31998  unipreima  32136  fpwrelmapffslem  32224  elirng  33039  esumfsup  33366  reprdifc  33937  bnj168  34039  bnj1398  34343  cvmliftlem15  34587  ellines  35428  bj-elsngl  36152  bj-dfmpoa  36302  ptrecube  36791  cnambfre  36839  islshpat  38190  lfl1dim  38294  glbconxN  38552  3dim0  38631  2dim  38644  1dimN  38645  islpln5  38709  islvol5  38753  dalem20  38867  lhpex2leN  39187  mapdval4N  40806  rexrabdioph  41834  rmxdioph  42057  expdiophlem1  42062  imaiun1  42704  coiun1  42705  ismnuprim  43355  prmunb2  43372  fourierdlem48  45168  2reuimp0  46120  2reuimp  46121  wtgoldbnnsum4prm  46768  bgoldbnnsum3prm  46770  islindeps2  47251  isldepslvec2  47253  sepnsepolem1  47641