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

Theorem reximdai 3243
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 3239 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3087 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1786  wcel 2107  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-ral 3062  df-rex 3071
This theorem is referenced by:  2reurex  3719  tz7.49  8392  hsmexlem2  10368  acunirnmpt2  31622  acunirnmpt2f  31623  locfinreflem  32478  cmpcref  32488  fvineqsneq  35929  indexdom  36239  filbcmb  36245  cdlemefr29exN  38911  rexanuz3  43394  reximdd  43450  disjrnmpt2  43495  fompt  43499  disjinfi  43500  iunmapsn  43525  infnsuprnmpt  43565  rnmptbdlem  43570  supxrge  43659  suplesup  43660  infxr  43688  allbutfi  43714  supxrunb3  43720  infxrunb3rnmpt  43749  infrpgernmpt  43786  limsupre  43968  limsupub  44031  limsupre3lem  44059  limsupgtlem  44104  xlimmnfvlem1  44159  xlimpnfvlem1  44163  stoweidlem31  44358  stoweidlem34  44361  fourierdlem73  44506  sge0pnffigt  44723  sge0ltfirp  44727  sge0reuzb  44775  iundjiun  44787  ovnlerp  44889  smflimlem4  45101  smflimsuplem7  45153
  Copyright terms: Public domain W3C validator