Theorem rexlimi 3238

Description: Restricted quantifier version of exlimi 2225. For a version based on fewer axioms see rexlimiv 3132. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Hypotheses

Ref	Expression
rexlimi.1	⊢ Ⅎ𝑥𝜓
rexlimi.2	⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))

Assertion

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

Proof of Theorem rexlimi

Step	Hyp	Ref	Expression
1		rexlimi.2	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	rgen 3054	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		rexlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	r19.23 3235	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
5	2, 4	mpbi 230	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053  df-rex 3063

This theorem is referenced by:  reuan  3835  triun  5207  reusv1  5334  reusv3  5342  iunopeqop  5469  tfinds  7804  fiun  7889  f1iun  7890  frpoins3xpg  8083  frpoins3xp3g  8084  iunfo  10452  iundom2g  10453  fsumcom2  15727  fprodcom2  15940  nosupbnd1  27692  nosupbnd2  27694  noinfbnd1  27707  noinfbnd2  27709  dfon2lem7  35985  finminlem  36516  r19.36vf  45584  allbutfiinf  45866  infxrunb3rnmpt  45874  hoidmvlelem1  47041  2zrngmmgm  48740