Theorem rexlimi 3232

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3048  df-rex 3057

This theorem is referenced by:  reuan  3847  triun  5212  reusv1  5335  reusv3  5343  iunopeqop  5461  tfinds  7790  fiun  7875  f1iun  7876  frpoins3xpg  8070  frpoins3xp3g  8071  iunfo  10430  iundom2g  10431  fsumcom2  15681  fprodcom2  15891  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2  27671  dfon2lem7  35829  finminlem  36358  r19.36vf  45179  allbutfiinf  45464  infxrunb3rnmpt  45472  hoidmvlelem1  46639  2zrngmmgm  48289