Theorem rexlimi 3248

Description: Restricted quantifier version of exlimi 2210. (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 3074	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		rexlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	r19.23 3247	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
5	2, 4	mpbi 229	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-ral 3069  df-rex 3070

This theorem is referenced by:  reuan  3829  triun  5204  reusv1  5320  reusv3  5328  iunopeqop  5435  tfinds  7706  fiun  7785  f1iun  7786  iunfo  10295  iundom2g  10296  fsumcom2  15486  fprodcom2  15694  dfon2lem7  33765  frpoins3xpg  33787  frpoins3xp3g  33788  nosupbnd1  33917  nosupbnd2  33919  noinfbnd1  33932  noinfbnd2  33934  finminlem  34507  r19.36vf  42685  allbutfiinf  42960  infxrunb3rnmpt  42968  hoidmvlelem1  44133  2zrngmmgm  45504