Theorem rexlimi 3238

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

Syntax hints:   → wi 4  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3046  df-rex 3055

This theorem is referenced by:  reuan  3862  triun  5232  reusv1  5355  reusv3  5363  iunopeqop  5484  tfinds  7839  fiun  7924  f1iun  7925  frpoins3xpg  8122  frpoins3xp3g  8123  iunfo  10499  iundom2g  10500  fsumcom2  15747  fprodcom2  15957  nosupbnd1  27633  nosupbnd2  27635  noinfbnd1  27648  noinfbnd2  27650  dfon2lem7  35784  finminlem  36313  r19.36vf  45137  allbutfiinf  45423  infxrunb3rnmpt  45431  hoidmvlelem1  46600  2zrngmmgm  48244