Theorem rexlimi 3239

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071

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 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3075  df-rex 3076

This theorem is referenced by:  reuan  3804  triun  5155  reusv1  5270  reusv3  5278  iunopeqop  5384  tfinds  7579  fiun  7654  f1iun  7655  iunfo  10012  iundom2g  10013  fsumcom2  15190  fprodcom2  15399  dfon2lem7  33293  frpoins3xpg  33344  frpoins3xp3g  33345  nosupbnd1  33514  nosupbnd2  33516  noinfbnd1  33529  noinfbnd2  33531  finminlem  34090  r19.36vf  42179  allbutfiinf  42458  infxrunb3rnmpt  42466  hoidmvlelem1  43635  2zrngmmgm  44986