Theorem rexlimi 3236

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

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060

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 2184

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

This theorem is referenced by:  reuan  3846  triun  5219  reusv1  5342  reusv3  5350  iunopeqop  5469  tfinds  7802  fiun  7887  f1iun  7888  frpoins3xpg  8082  frpoins3xp3g  8083  iunfo  10449  iundom2g  10450  fsumcom2  15697  fprodcom2  15907  nosupbnd1  27682  nosupbnd2  27684  noinfbnd1  27697  noinfbnd2  27699  dfon2lem7  35981  finminlem  36512  r19.36vf  45376  allbutfiinf  45660  infxrunb3rnmpt  45668  hoidmvlelem1  46835  2zrngmmgm  48494