Theorem r19.42v 3169

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  ceqsrexbv  3598  ceqsrex2v  3600  2reuswap  3692  2reuswap2  3693  2reu5  3704  2rmoswap  3707  dfiun2g  4972  iunrab  4995  iunin2  5013  iundif2  5016  reusv2lem4  5343  iunopab  5514  cnvuni  5841  elidinxp  6009  xpdifid  6132  dfpo2  6260  elunirn  7206  f1oiso  7306  oprabrexex2  7931  oeeu  8539  trcl  9649  dfac5lem2  10046  axgroth4  10755  rexuz2  12849  4fvwrd4  13602  divalglem10  16371  divalgb  16373  lsmelval2  21080  tgcmp  23366  hauscmplem  23371  unisngl  23492  xkobval  23551  txtube  23605  txcmplem1  23606  txkgen  23617  xkococnlem  23624  mbfaddlem  25627  mbfsup  25631  elaa  26282  dchrisumlem3  27454  elold  27851  colperpexlem3  28800  midex  28805  iscgra1  28878  ax5seg  29007  edglnl  29212  usgr2pth0  29833  hhcmpl  31271  sumdmdii  32486  reuxfrdf  32560  unipreima  32716  fpwrelmapffslem  32805  elirng  33830  esumfsup  34214  reprdifc  34771  bnj168  34873  bnj1398  35176  cvmliftlem15  35480  ellines  36334  bj-elsngl  37275  bj-dfmpoa  37430  ptrecube  37941  cnambfre  37989  islshpat  39463  lfl1dim  39567  glbconxN  39824  3dim0  39903  2dim  39916  1dimN  39917  islpln5  39981  islvol5  40025  dalem20  40139  lhpex2leN  40459  mapdval4N  42078  rexrabdioph  43222  rmxdioph  43444  expdiophlem1  43449  imaiun1  44078  coiun1  44079  ismnuprim  44721  prmunb2  44738  fourierdlem48  46582  2reuimp0  47562  2reuimp  47563  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  dfvopnbgr2  48329  stgredgiun  48434  islindeps2  48959  isldepslvec2  48961  sepnsepolem1  49397