Theorem r19.42v 3197

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexcomOLD  3297  ceqsrexbv  3669  ceqsrex2v  3671  2reuswap  3768  2reuswap2  3769  2reu5  3780  2rmoswap  3783  dfiun2g  5053  iunrab  5075  iunin2  5094  iundif2  5097  reusv2lem4  5419  iunopab  5578  iunopabOLD  5579  cnvuni  5911  elidinxp  6073  xpdifid  6199  dfpo2  6327  elunirn  7288  f1oiso  7387  oprabrexex2  8019  oeeu  8659  trcl  9797  dfac5lem2  10193  axgroth4  10901  rexuz2  12964  4fvwrd4  13705  cshwsexaOLD  14873  divalglem10  16450  divalgb  16452  lsmelval2  21107  tgcmp  23430  hauscmplem  23435  unisngl  23556  xkobval  23615  txtube  23669  txcmplem1  23670  txkgen  23681  xkococnlem  23688  mbfaddlem  25714  mbfsup  25718  elaa  26376  dchrisumlem3  27553  elold  27926  0reno  28447  colperpexlem3  28758  midex  28763  iscgra1  28836  ax5seg  28971  edglnl  29178  usgr2pth0  29801  hhcmpl  31232  sumdmdii  32447  reuxfrdf  32519  unipreima  32662  fpwrelmapffslem  32746  elirng  33686  esumfsup  34034  reprdifc  34604  bnj168  34706  bnj1398  35010  cvmliftlem15  35266  ellines  36116  bj-elsngl  36934  bj-dfmpoa  37084  ptrecube  37580  cnambfre  37628  islshpat  38973  lfl1dim  39077  glbconxN  39335  3dim0  39414  2dim  39427  1dimN  39428  islpln5  39492  islvol5  39536  dalem20  39650  lhpex2leN  39970  mapdval4N  41589  rexrabdioph  42750  rmxdioph  42973  expdiophlem1  42978  imaiun1  43613  coiun1  43614  ismnuprim  44263  prmunb2  44280  fourierdlem48  46075  2reuimp0  47029  2reuimp  47030  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  dfvopnbgr2  47725  islindeps2  48212  isldepslvec2  48214  sepnsepolem1  48601