Theorem rexlimi 3268

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3083  df-rex 3093

This theorem is used by:  reuan  3853  triun  5238  reusv1  5373  reusv3  5381  iunopeqop  5509  iunopeqopOLD  5510  tfinds  7865  fiun  7949  f1iun  7950  frpoins3xpg  8145  frpoins3xp3g  8146  iunfo  10541  iundom2g  10542  fsumcom2  15851  fprodcom2  16064  nosupbnd1  27915  nosupbnd2  27917  noinfbnd1  27930  noinfbnd2  27932  dfon2lem7  36299  finminlem  36869  r19.36vf  45894  allbutfiinf  46174  infxrunb3rnmpt  46182  hoidmvlelem1  47349  2zrngmmgm  49057