Theorem rexlimi 3240

Description: Restricted quantifier version of exlimi 2229. For a version based on fewer axioms see rexlimiv 3134. (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 3056	. 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓)
3		rexlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
4	3	r19.23 3237	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓))
5	2, 4	mpbi 231	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1790   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791  df-ral 3055  df-rex 3065

This theorem is referenced by:  reuan  3835  triun  5201  reusv1  5333  reusv3  5341  iunopeqop  5469  iunopeqopOLD  5470  tfinds  7807  fiun  7892  f1iun  7893  frpoins3xpg  8087  frpoins3xp3g  8088  iunfo  10459  iundom2g  10460  fsumcom2  15734  fprodcom2  15947  nosupbnd1  27703  nosupbnd2  27705  noinfbnd1  27718  noinfbnd2  27720  dfon2lem7  36022  finminlem  36553  r19.36vf  45590  allbutfiinf  45870  infxrunb3rnmpt  45878  hoidmvlelem1  47045  2zrngmmgm  48750