Theorem rexlimi 3266

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3081  df-rex 3091

This theorem is used by:  reuan  3848  triun  5230  reusv1  5363  reusv3  5371  iunopeqop  5498  iunopeqopOLD  5499  tfinds  7895  fiun  7979  f1iun  7980  frpoins3xpg  8184  frpoins3xp3g  8185  iunfo  10650  iundom2g  10651  fsumcom2  15969  fprodcom2  16180  nosupbnd1  28101  nosupbnd2  28103  noinfbnd1  28116  noinfbnd2  28118  dfon2lem7  36729  finminlem  37284  r19.36vf  46356  allbutfiinf  46635  infxrunb3rnmpt  46643  hoidmvlelem1  47810  2zrngmmgm  49554