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  8159  frpoins3xp3g  8160  iunfo  10626  iundom2g  10627  fsumcom2  15945  fprodcom2  16156  nosupbnd1  28076  nosupbnd2  28078  noinfbnd1  28091  noinfbnd2  28093  dfon2lem7  36643  finminlem  37198  r19.36vf  46244  allbutfiinf  46523  infxrunb3rnmpt  46531  hoidmvlelem1  47698  2zrngmmgm  49442