Theorem r19.42v 3176

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 3174	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
2		ancom 460	. . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑))
3	2	rexbii 3083	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑))
4		ancom 460	. 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓))

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

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 3061

This theorem is referenced by:  rexcomOLD  3272  ceqsrexbv  3635  ceqsrex2v  3637  2reuswap  3729  2reuswap2  3730  2reu5  3741  2rmoswap  3744  dfiun2g  5006  iunrab  5028  iunin2  5047  iundif2  5050  reusv2lem4  5371  iunopab  5534  iunopabOLD  5535  cnvuni  5866  elidinxp  6031  xpdifid  6157  dfpo2  6285  elunirn  7243  f1oiso  7344  oprabrexex2  7977  oeeu  8615  trcl  9742  dfac5lem2  10138  axgroth4  10846  rexuz2  12915  4fvwrd4  13665  cshwsexaOLD  14843  divalglem10  16421  divalgb  16423  lsmelval2  21043  tgcmp  23339  hauscmplem  23344  unisngl  23465  xkobval  23524  txtube  23578  txcmplem1  23579  txkgen  23590  xkococnlem  23597  mbfaddlem  25613  mbfsup  25617  elaa  26276  dchrisumlem3  27454  elold  27833  0reno  28400  colperpexlem3  28711  midex  28716  iscgra1  28789  ax5seg  28917  edglnl  29122  usgr2pth0  29747  hhcmpl  31181  sumdmdii  32396  reuxfrdf  32472  unipreima  32621  fpwrelmapffslem  32709  elirng  33727  esumfsup  34101  reprdifc  34659  bnj168  34761  bnj1398  35065  cvmliftlem15  35320  ellines  36170  bj-elsngl  36986  bj-dfmpoa  37136  ptrecube  37644  cnambfre  37692  islshpat  39035  lfl1dim  39139  glbconxN  39397  3dim0  39476  2dim  39489  1dimN  39490  islpln5  39554  islvol5  39598  dalem20  39712  lhpex2leN  40032  mapdval4N  41651  rexrabdioph  42817  rmxdioph  43040  expdiophlem1  43045  imaiun1  43675  coiun1  43676  ismnuprim  44318  prmunb2  44335  fourierdlem48  46183  2reuimp0  47143  2reuimp  47144  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  dfvopnbgr2  47866  stgredgiun  47970  islindeps2  48459  isldepslvec2  48461  sepnsepolem1  48896