Theorem rexlimiva 2618

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)

Hypothesis

Ref	Expression
rexlimiva.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
rexlimiva	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
2	1	ex 115	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 2617	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2176  ∃wrex 2485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  unon  4559  reg2exmidlema  4582  ssfilem  6972  diffitest  6984  fival  7072  elfi2  7074  fi0  7077  djuss  7172  updjud  7184  enumct  7217  finnum  7290  dmaddpqlem  7490  nqpi  7491  nq0nn  7555  recexprlemm  7737  iswrd  10996  wrdf  11000  rexanuz  11299  r19.2uz  11304  maxleast  11524  fsum2dlemstep  11745  fisumcom2  11749  fprod2dlemstep  11933  fprodcom2fi  11937  0dvds  12122  even2n  12185  m1expe  12210  m1exp1  12212  modprm0  12577  gsumval2  13229  dfgrp2  13359  epttop  14562  neipsm  14626  tgioo  15026  sin0pilem2  15254  pilem3  15255  perfect  15473  bj-nn0suc  15900  bj-nn0sucALT  15914  trirec0xor  15984