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

Theorem reximdai 3308
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 3213 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3238 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1775  wcel 2105  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-ral 3140  df-rex 3141
This theorem is referenced by:  2reurex  3747  tz7.49  8070  hsmexlem2  9837  acunirnmpt2  30333  acunirnmpt2f  30334  locfinreflem  31003  cmpcref  31013  fvineqsneq  34575  indexdom  34890  filbcmb  34896  cdlemefr29exN  37418  rexanuz3  41239  reximdd  41297  disjrnmpt2  41325  fompt  41329  disjinfi  41330  iunmapsn  41356  infnsuprnmpt  41398  rnmptbdlem  41403  supxrge  41482  suplesup  41483  infxr  41511  allbutfi  41541  supxrunb3  41548  infxrunb3rnmpt  41578  infrpgernmpt  41617  limsupre  41798  limsupub  41861  limsupre3lem  41889  limsupgtlem  41934  xlimmnfvlem1  41989  xlimpnfvlem1  41993  stoweidlem31  42193  stoweidlem34  42196  fourierdlem73  42341  sge0pnffigt  42555  sge0ltfirp  42559  sge0reuzb  42607  iundjiun  42619  ovnlerp  42721  smflimlem4  42927  smflimsuplem7  42977
  Copyright terms: Public domain W3C validator