Theorem rexlimi 3262

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077  df-rex 3087

This theorem is used by:  reuan  3843  triun  5226  reusv1  5358  reusv3  5366  iunopeqop  5493  iunopeqopOLD  5494  tfinds  7871  fiun  7955  f1iun  7956  frpoins3xpg  8157  frpoins3xp3g  8158  iunfo  10624  iundom2g  10625  fsumcom2  15941  fprodcom2  16152  nosupbnd1  28072  nosupbnd2  28074  noinfbnd1  28087  noinfbnd2  28089  dfon2lem7  36594  finminlem  37149  r19.36vf  46195  allbutfiinf  46474  infxrunb3rnmpt  46482  hoidmvlelem1  47649  2zrngmmgm  49393