Theorem rexim 3168

Description: Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
rexim	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))

Proof of Theorem rexim

Step	Hyp	Ref	Expression
1		con3 153	. . . 4 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))
2	1	ral2imi 3081	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 ¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
3	2	con3d 152	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑 → ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜓))
4		dfrex2 3166	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
5		dfrex2 3166	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜓)
6	3, 4, 5	3imtr4g 295	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4  ∀wral 3063  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexbi  3169  reximiaOLD  3173  r19.29  3183  reximdvaiOLD  3200  reximdai  3239  r19.30  3265  r19.35  3268  reupick2  4251  ss2iun  4939  chfnrn  6908  isf32lem2  10041  ptcmplem4  23114  bnj110  32738  madebdayim  33997  madebdaylemold  34005  poimirlem25  35729