Theorem rexlimi 3264

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3078  ∃wrex 3088

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 1943  ax-6 2000  ax-7 2041  ax-12 2215

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

This theorem is used by:  reuan  3847  triun  5231  reusv1  5366  reusv3  5374  iunopeqop  5502  iunopeqopOLD  5503  tfinds  7860  fiun  7944  f1iun  7945  frpoins3xpg  8142  frpoins3xp3g  8143  iunfo  10551  iundom2g  10552  fsumcom2  15864  fprodcom2  16077  nosupbnd1  27958  nosupbnd2  27960  noinfbnd1  27973  noinfbnd2  27975  dfon2lem7  36374  finminlem  36945  r19.36vf  45976  allbutfiinf  46256  infxrunb3rnmpt  46264  hoidmvlelem1  47431  2zrngmmgm  49175