Theorem rexlimi 3265

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

Syntax hints:   → wi 4  Ⅎwnf 1813   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814  df-ral 3080  df-rex 3090

This theorem is referenced by:  reuan  3851  triun  5234  reusv1  5370  reusv3  5378  iunopeqop  5506  iunopeqopOLD  5507  tfinds  7857  fiun  7941  f1iun  7942  frpoins3xpg  8137  frpoins3xp3g  8138  iunfo  10524  iundom2g  10525  fsumcom2  15827  fprodcom2  16040  nosupbnd1  27856  nosupbnd2  27858  noinfbnd1  27871  noinfbnd2  27873  dfon2lem7  36257  finminlem  36807  r19.36vf  45834  allbutfiinf  46114  infxrunb3rnmpt  46122  hoidmvlelem1  47289  2zrngmmgm  48994