Theorem rexim 3070

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 3068	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∀𝑥 ∈ 𝐴 ¬ 𝜓 → ∀𝑥 ∈ 𝐴 ¬ 𝜑))
3		ralnex 3055	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4		ralnex 3055	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜑)
5	2, 3, 4	3imtr3g 295	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (¬ ∃𝑥 ∈ 𝐴 𝜓 → ¬ ∃𝑥 ∈ 𝐴 𝜑))
6	5	con4d 115	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4  ∀wral 3044  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  rexbi  3086  r19.35OLD  3089  r19.29OLD  3095  r19.30  3100  reximdai  3239  reupick2  4294  ss2iun  4974  dfiun2g  4994  chfnrn  7021  isf32lem2  10307  psdmul  22053  ptcmplem4  23942  madebdayim  27799  madebdaylemold  27809  bnj110  34848  poimirlem25  37639