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

Theorem reximdai 3297
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 3205 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3229 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1785  wcel 2114  wral 3130  wrex 3131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2178
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3135  df-rex 3136
This theorem is referenced by:  2reurex  3725  tz7.49  8068  hsmexlem2  9838  acunirnmpt2  30413  acunirnmpt2f  30414  locfinreflem  31162  cmpcref  31172  fvineqsneq  34790  indexdom  35130  filbcmb  35136  cdlemefr29exN  37656  rexanuz3  41668  reximdd  41726  disjrnmpt2  41753  fompt  41757  disjinfi  41758  iunmapsn  41784  infnsuprnmpt  41826  rnmptbdlem  41831  supxrge  41909  suplesup  41910  infxr  41938  allbutfi  41968  supxrunb3  41975  infxrunb3rnmpt  42004  infrpgernmpt  42043  limsupre  42222  limsupub  42285  limsupre3lem  42313  limsupgtlem  42358  xlimmnfvlem1  42413  xlimpnfvlem1  42417  stoweidlem31  42612  stoweidlem34  42615  fourierdlem73  42760  sge0pnffigt  42974  sge0ltfirp  42978  sge0reuzb  43026  iundjiun  43038  ovnlerp  43140  smflimlem4  43346  smflimsuplem7  43396
  Copyright terms: Public domain W3C validator