Theorem r19.42v 3169

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 3167	. 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  3622  ceqsrex2v  3624  2reuswap  3717  2reuswap2  3718  2reu5  3729  2rmoswap  3732  dfiun2g  4994  iunrab  5016  iunin2  5035  iundif2  5038  reusv2lem4  5356  iunopab  5519  iunopabOLD  5520  cnvuni  5850  elidinxp  6015  xpdifid  6141  dfpo2  6269  elunirn  7225  f1oiso  7326  oprabrexex2  7957  oeeu  8567  trcl  9681  dfac5lem2  10077  axgroth4  10785  rexuz2  12858  4fvwrd4  13609  cshwsexaOLD  14790  divalglem10  16372  divalgb  16374  lsmelval2  20992  tgcmp  23288  hauscmplem  23293  unisngl  23414  xkobval  23473  txtube  23527  txcmplem1  23528  txkgen  23539  xkococnlem  23546  mbfaddlem  25561  mbfsup  25565  elaa  26224  dchrisumlem3  27402  elold  27781  0reno  28348  colperpexlem3  28659  midex  28664  iscgra1  28737  ax5seg  28865  edglnl  29070  usgr2pth0  29695  hhcmpl  31129  sumdmdii  32344  reuxfrdf  32420  unipreima  32567  fpwrelmapffslem  32655  elirng  33681  esumfsup  34060  reprdifc  34618  bnj168  34720  bnj1398  35024  cvmliftlem15  35285  ellines  36140  bj-elsngl  36956  bj-dfmpoa  37106  ptrecube  37614  cnambfre  37662  islshpat  39010  lfl1dim  39114  glbconxN  39372  3dim0  39451  2dim  39464  1dimN  39465  islpln5  39529  islvol5  39573  dalem20  39687  lhpex2leN  40007  mapdval4N  41626  rexrabdioph  42782  rmxdioph  43005  expdiophlem1  43010  imaiun1  43640  coiun1  43641  ismnuprim  44283  prmunb2  44300  fourierdlem48  46152  2reuimp0  47115  2reuimp  47116  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  dfvopnbgr2  47853  stgredgiun  47957  islindeps2  48472  isldepslvec2  48474  sepnsepolem1  48910