Theorem r19.42v 3166

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  ceqsrexbv  3608  ceqsrex2v  3610  2reuswap  3702  2reuswap2  3703  2reu5  3714  2rmoswap  3717  dfiun2g  4983  iunrab  5006  iunin2  5024  iundif2  5027  reusv2lem4  5344  iunopab  5505  cnvuni  5833  elidinxp  6001  xpdifid  6124  dfpo2  6252  elunirn  7195  f1oiso  7295  oprabrexex2  7920  oeeu  8529  trcl  9635  dfac5lem2  10032  axgroth4  10741  rexuz2  12810  4fvwrd4  13562  divalglem10  16327  divalgb  16329  lsmelval2  21035  tgcmp  23343  hauscmplem  23348  unisngl  23469  xkobval  23528  txtube  23582  txcmplem1  23583  txkgen  23594  xkococnlem  23601  mbfaddlem  25615  mbfsup  25619  elaa  26278  dchrisumlem3  27456  elold  27841  colperpexlem3  28753  midex  28758  iscgra1  28831  ax5seg  28960  edglnl  29165  usgr2pth0  29787  hhcmpl  31224  sumdmdii  32439  reuxfrdf  32514  unipreima  32670  fpwrelmapffslem  32760  elirng  33792  esumfsup  34176  reprdifc  34733  bnj168  34835  bnj1398  35139  cvmliftlem15  35441  ellines  36295  bj-elsngl  37112  bj-dfmpoa  37262  ptrecube  37760  cnambfre  37808  islshpat  39216  lfl1dim  39320  glbconxN  39577  3dim0  39656  2dim  39669  1dimN  39670  islpln5  39734  islvol5  39778  dalem20  39892  lhpex2leN  40212  mapdval4N  41831  rexrabdioph  42978  rmxdioph  43200  expdiophlem1  43205  imaiun1  43834  coiun1  43835  ismnuprim  44477  prmunb2  44494  fourierdlem48  46340  2reuimp0  47302  2reuimp  47303  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  dfvopnbgr2  48041  stgredgiun  48146  islindeps2  48671  isldepslvec2  48673  sepnsepolem1  49109