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

Theorem reximdai 3254
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 3166 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3188 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1746  wcel 2050  wral 3088  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-12 2106
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747  df-ral 3093  df-rex 3094
This theorem is referenced by:  2reurex  3661  tz7.49  7886  hsmexlem2  9649  acunirnmpt2  30170  acunirnmpt2f  30171  locfinreflem  30748  cmpcref  30758  fvineqsneq  34134  indexdom  34451  filbcmb  34457  cdlemefr29exN  36983  rexanuz3  40785  reximdd  40844  disjrnmpt2  40874  fompt  40878  disjinfi  40879  iunmapsn  40906  infnsuprnmpt  40951  rnmptbdlem  40956  supxrge  41036  suplesup  41037  infxr  41065  allbutfi  41096  supxrunb3  41103  infxrunb3rnmpt  41134  infrpgernmpt  41173  limsupre  41354  limsupub  41417  limsupre3lem  41445  limsupgtlem  41490  xlimmnfvlem1  41545  xlimpnfvlem1  41549  stoweidlem31  41748  stoweidlem34  41751  fourierdlem73  41896  sge0pnffigt  42110  sge0ltfirp  42114  sge0reuzb  42162  iundjiun  42174  ovnlerp  42276  smflimlem4  42482  smflimsuplem7  42532
  Copyright terms: Public domain W3C validator