Theorem rexlimi 3263

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087

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 2213

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

This theorem is used by:  reuan  3844  triun  5227  reusv1  5359  reusv3  5367  iunopeqop  5494  iunopeqopOLD  5495  tfinds  7860  fiun  7944  f1iun  7945  frpoins3xpg  8141  frpoins3xp3g  8142  iunfo  10604  iundom2g  10605  fsumcom2  15920  fprodcom2  16131  nosupbnd1  28053  nosupbnd2  28055  noinfbnd1  28068  noinfbnd2  28070  dfon2lem7  36521  finminlem  37076  r19.36vf  46094  allbutfiinf  46374  infxrunb3rnmpt  46382  hoidmvlelem1  47549  2zrngmmgm  49293