Theorem rexim 3087

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

Syntax hints:  ¬ wn 3   → wi 4  ∀wral 3061  ∃wrex 3070

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 3062  df-rex 3071

This theorem is referenced by:  reximiaOLD  3088  rexbi  3104  r19.35OLD  3109  r19.29OLD  3115  r19.30  3120  reximdvaiOLD  3166  reximdai  3261  reupick2  4331  ss2iun  5010  dfiun2g  5030  chfnrn  7069  isf32lem2  10394  psdmul  22170  ptcmplem4  24063  madebdayim  27926  madebdaylemold  27936  bnj110  34872  poimirlem25  37652