MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexim Structured version   Visualization version   GIF version

Theorem rexim 3085
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
StepHypRef Expression
1 con3 153 . . . 4 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
21ral2imi 3083 . . 3 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
3 ralnex 3070 . . 3 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
4 ralnex 3070 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
52, 3, 43imtr3g 295 . 2 (∀𝑥𝐴 (𝜑𝜓) → (¬ ∃𝑥𝐴 𝜓 → ¬ ∃𝑥𝐴 𝜑))
65con4d 115 1 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wral 3059  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069
This theorem is referenced by:  reximiaOLD  3086  rexbi  3102  r19.35OLD  3107  r19.29OLD  3113  r19.30  3118  reximdvaiOLD  3164  reximdai  3259  reupick2  4337  ss2iun  5015  dfiun2g  5035  chfnrn  7069  isf32lem2  10392  psdmul  22188  ptcmplem4  24079  madebdayim  27941  madebdaylemold  27951  bnj110  34851  poimirlem25  37632
  Copyright terms: Public domain W3C validator