Theorem r19.42v 3188

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068

This theorem is referenced by:  rexcomOLD  3286  ceqsrexbv  3644  ceqsrex2v  3646  2reuswap  3743  2reuswap2  3744  2reu5  3755  2rmoswap  3758  dfiun2g  5037  iunrab  5059  iunin2  5078  iundif2  5081  reusv2lem4  5405  iunopab  5565  iunopabOLD  5566  cnvuni  5893  elidinxp  6052  xpdifid  6177  dfpo2  6305  elunirn  7267  f1oiso  7365  oprabrexex2  7988  oeeu  8630  trcl  9759  dfac5lem2  10155  axgroth4  10863  rexuz2  12921  4fvwrd4  13661  cshwsexaOLD  14815  divalglem10  16386  divalgb  16388  lsmelval2  20977  tgcmp  23325  hauscmplem  23330  unisngl  23451  xkobval  23510  txtube  23564  txcmplem1  23565  txkgen  23576  xkococnlem  23583  mbfaddlem  25609  mbfsup  25613  elaa  26271  dchrisumlem3  27444  elold  27816  0reno  28245  colperpexlem3  28556  midex  28561  iscgra1  28634  ax5seg  28769  edglnl  28976  usgr2pth0  29599  hhcmpl  31030  sumdmdii  32245  reuxfrdf  32310  unipreima  32451  fpwrelmapffslem  32535  elirng  33397  esumfsup  33722  reprdifc  34292  bnj168  34394  bnj1398  34698  cvmliftlem15  34941  ellines  35781  bj-elsngl  36480  bj-dfmpoa  36630  ptrecube  37126  cnambfre  37174  islshpat  38521  lfl1dim  38625  glbconxN  38883  3dim0  38962  2dim  38975  1dimN  38976  islpln5  39040  islvol5  39084  dalem20  39198  lhpex2leN  39518  mapdval4N  41137  rexrabdioph  42245  rmxdioph  42468  expdiophlem1  42473  imaiun1  43112  coiun1  43113  ismnuprim  43762  prmunb2  43779  fourierdlem48  45571  2reuimp0  46523  2reuimp  46524  wtgoldbnnsum4prm  47171  bgoldbnnsum3prm  47173  dfvopnbgr2  47217  islindeps2  47629  isldepslvec2  47631  sepnsepolem1  48018