Theorem r19.42v 3167

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

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

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 3054

This theorem is referenced by:  ceqsrexbv  3619  ceqsrex2v  3621  2reuswap  3714  2reuswap2  3715  2reu5  3726  2rmoswap  3729  dfiun2g  4990  iunrab  5011  iunin2  5030  iundif2  5033  reusv2lem4  5351  iunopab  5514  cnvuni  5840  elidinxp  6004  xpdifid  6129  dfpo2  6257  elunirn  7207  f1oiso  7308  oprabrexex2  7936  oeeu  8544  trcl  9657  dfac5lem2  10053  axgroth4  10761  rexuz2  12834  4fvwrd4  13585  cshwsexaOLD  14766  divalglem10  16348  divalgb  16350  lsmelval2  21024  tgcmp  23321  hauscmplem  23326  unisngl  23447  xkobval  23506  txtube  23560  txcmplem1  23561  txkgen  23572  xkococnlem  23579  mbfaddlem  25594  mbfsup  25598  elaa  26257  dchrisumlem3  27435  elold  27818  0reno  28401  colperpexlem3  28712  midex  28717  iscgra1  28790  ax5seg  28918  edglnl  29123  usgr2pth0  29745  hhcmpl  31179  sumdmdii  32394  reuxfrdf  32470  unipreima  32617  fpwrelmapffslem  32705  elirng  33674  esumfsup  34053  reprdifc  34611  bnj168  34713  bnj1398  35017  cvmliftlem15  35278  ellines  36133  bj-elsngl  36949  bj-dfmpoa  37099  ptrecube  37607  cnambfre  37655  islshpat  39003  lfl1dim  39107  glbconxN  39365  3dim0  39444  2dim  39457  1dimN  39458  islpln5  39522  islvol5  39566  dalem20  39680  lhpex2leN  40000  mapdval4N  41619  rexrabdioph  42775  rmxdioph  42998  expdiophlem1  43003  imaiun1  43633  coiun1  43634  ismnuprim  44276  prmunb2  44293  fourierdlem48  46145  2reuimp0  47108  2reuimp  47109  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  dfvopnbgr2  47846  stgredgiun  47950  islindeps2  48465  isldepslvec2  48467  sepnsepolem1  48903