Theorem rexlimi 3238

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

Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053  df-rex 3063

This theorem is referenced by:  reuan  3848  triun  5221  reusv1  5344  reusv3  5352  iunopeqop  5477  tfinds  7812  fiun  7897  f1iun  7898  frpoins3xpg  8092  frpoins3xp3g  8093  iunfo  10461  iundom2g  10462  fsumcom2  15709  fprodcom2  15919  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2  27711  dfon2lem7  36000  finminlem  36531  r19.36vf  45489  allbutfiinf  45772  infxrunb3rnmpt  45780  hoidmvlelem1  46947  2zrngmmgm  48606