Theorem rexlimi 3256

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

Syntax hints:   → wi 4  Ⅎwnf 1779   ∈ wcel 2105  ∀wral 3058  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-ral 3059  df-rex 3068

This theorem is referenced by:  reuan  3904  triun  5279  reusv1  5402  reusv3  5410  iunopeqop  5530  tfinds  7880  fiun  7965  f1iun  7966  frpoins3xpg  8163  frpoins3xp3g  8164  iunfo  10576  iundom2g  10577  fsumcom2  15806  fprodcom2  16016  nosupbnd1  27773  nosupbnd2  27775  noinfbnd1  27788  noinfbnd2  27790  dfon2lem7  35770  finminlem  36300  r19.36vf  45075  allbutfiinf  45369  infxrunb3rnmpt  45377  hoidmvlelem1  46550  2zrngmmgm  48095