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

Theorem reximdai 3158
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 31-Aug-1999.)
Hypotheses
Ref Expression
reximdai.1 𝑥𝜑
reximdai.2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
Assertion
Ref Expression
reximdai (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))

Proof of Theorem reximdai
StepHypRef Expression
1 reximdai.1 . . 3 𝑥𝜑
2 reximdai.2 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
31, 2ralrimi 3104 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3154 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1878  wcel 2155  wral 3055  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-nf 1879  df-ral 3060  df-rex 3061
This theorem is referenced by:  tz7.49  7744  hsmexlem2  9502  acunirnmpt2  29910  acunirnmpt2f  29911  locfinreflem  30354  cmpcref  30364  indexdom  33952  filbcmb  33958  cdlemefr29exN  36358  rexanuz3  39926  reximdd  39991  disjrnmpt2  40022  fompt  40026  disjinfi  40027  iunmapsn  40054  infnsuprnmpt  40106  rnmptbdlem  40111  supxrge  40192  suplesup  40193  infxr  40221  allbutfi  40253  supxrunb3  40260  infxrunb3rnmpt  40292  infrpgernmpt  40332  limsupre  40511  limsupub  40574  limsupre3lem  40602  limsupgtlem  40647  xlimmnfvlem1  40696  xlimpnfvlem1  40700  stoweidlem31  40885  stoweidlem34  40888  fourierdlem73  41033  sge0pnffigt  41250  sge0ltfirp  41254  sge0reuzb  41302  iundjiun  41314  ovnlerp  41416  smflimlem4  41622  smflimsuplem7  41672  2reurex  41852
  Copyright terms: Public domain W3C validator