Theorem r19.42v 3188

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexcomOLD  3288  ceqsrexbv  3655  ceqsrex2v  3657  2reuswap  3754  2reuswap2  3755  2reu5  3766  2rmoswap  3769  dfiun2g  5034  iunrab  5056  iunin2  5075  iundif2  5078  reusv2lem4  5406  iunopab  5568  iunopabOLD  5569  cnvuni  5899  elidinxp  6063  xpdifid  6189  dfpo2  6317  elunirn  7270  f1oiso  7370  oprabrexex2  8001  oeeu  8639  trcl  9765  dfac5lem2  10161  axgroth4  10869  rexuz2  12938  4fvwrd4  13684  cshwsexaOLD  14859  divalglem10  16435  divalgb  16437  lsmelval2  21101  tgcmp  23424  hauscmplem  23429  unisngl  23550  xkobval  23609  txtube  23663  txcmplem1  23664  txkgen  23675  xkococnlem  23682  mbfaddlem  25708  mbfsup  25712  elaa  26372  dchrisumlem3  27549  elold  27922  0reno  28443  colperpexlem3  28754  midex  28759  iscgra1  28832  ax5seg  28967  edglnl  29174  usgr2pth0  29797  hhcmpl  31228  sumdmdii  32443  reuxfrdf  32518  unipreima  32659  fpwrelmapffslem  32749  elirng  33700  esumfsup  34050  reprdifc  34620  bnj168  34722  bnj1398  35026  cvmliftlem15  35282  ellines  36133  bj-elsngl  36950  bj-dfmpoa  37100  ptrecube  37606  cnambfre  37654  islshpat  38998  lfl1dim  39102  glbconxN  39360  3dim0  39439  2dim  39452  1dimN  39453  islpln5  39517  islvol5  39561  dalem20  39675  lhpex2leN  39995  mapdval4N  41614  rexrabdioph  42781  rmxdioph  43004  expdiophlem1  43009  imaiun1  43640  coiun1  43641  ismnuprim  44289  prmunb2  44306  fourierdlem48  46109  2reuimp0  47063  2reuimp  47064  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  dfvopnbgr2  47776  stgredgiun  47860  islindeps2  48328  isldepslvec2  48330  sepnsepolem1  48717