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

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
StepHypRef Expression
1 con3 153 . . . 4 ((𝜑𝜓) → (¬ 𝜓 → ¬ 𝜑))
21ral2imi 3085 . . 3 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 ¬ 𝜑))
3 ralnex 3072 . . 3 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
4 ralnex 3072 . . 3 (∀𝑥𝐴 ¬ 𝜑 ↔ ¬ ∃𝑥𝐴 𝜑)
52, 3, 43imtr3g 295 . 2 (∀𝑥𝐴 (𝜑𝜓) → (¬ ∃𝑥𝐴 𝜓 → ¬ ∃𝑥𝐴 𝜑))
65con4d 115 1 (∀𝑥𝐴 (𝜑𝜓) → (∃𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜓))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator