Theorem rexlimi 3237

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3045  df-rex 3054

This theorem is referenced by:  reuan  3859  triun  5229  reusv1  5352  reusv3  5360  iunopeqop  5481  tfinds  7836  fiun  7921  f1iun  7922  frpoins3xpg  8119  frpoins3xp3g  8120  iunfo  10492  iundom2g  10493  fsumcom2  15740  fprodcom2  15950  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  dfon2lem7  35777  finminlem  36306  r19.36vf  45130  allbutfiinf  45416  infxrunb3rnmpt  45424  hoidmvlelem1  46593  2zrngmmgm  48240