Theorem rexlimi 3257

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

Syntax hints:   → wi 4  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071

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 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3063  df-rex 3072

This theorem is referenced by:  reuan  3891  triun  5281  reusv1  5396  reusv3  5404  iunopeqop  5522  tfinds  7849  fiun  7929  f1iun  7930  frpoins3xpg  8126  frpoins3xp3g  8127  iunfo  10534  iundom2g  10535  fsumcom2  15720  fprodcom2  15928  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  dfon2lem7  34761  finminlem  35203  r19.36vf  43825  allbutfiinf  44130  infxrunb3rnmpt  44138  hoidmvlelem1  45311  2zrngmmgm  46844