Theorem rexlimi 3233

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2182

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3049  df-rex 3058

This theorem is referenced by:  reuan  3843  triun  5214  reusv1  5337  reusv3  5345  iunopeqop  5464  tfinds  7796  fiun  7881  f1iun  7882  frpoins3xpg  8076  frpoins3xp3g  8077  iunfo  10437  iundom2g  10438  fsumcom2  15683  fprodcom2  15893  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2  27671  dfon2lem7  35852  finminlem  36383  r19.36vf  45258  allbutfiinf  45543  infxrunb3rnmpt  45551  hoidmvlelem1  46718  2zrngmmgm  48377