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

Theorem rexim 3172
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 3082 . . 3 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
3 ralnex 3167 . . 3 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
4 ralnex 3167 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
52, 3, 43imtr3g 295 . 2 (∀𝑥𝐴 (𝜑𝜓) → (¬ ∃𝑥𝐴 𝜓 → ¬ ∃𝑥𝐴 𝜑))
65con4d 115 1 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wral 3064  wrex 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070
This theorem is referenced by:  rexbi  3173  reximiaOLD  3177  r19.29  3184  reximdvaiOLD  3201  reximdai  3244  r19.30  3268  r19.35  3271  reupick2  4254  ss2iun  4942  dfiun2g  4960  chfnrn  6926  isf32lem2  10110  ptcmplem4  23206  bnj110  32838  madebdayim  34070  madebdaylemold  34078  poimirlem25  35802
  Copyright terms: Public domain W3C validator