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

Theorem reximdai 3011
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 2956 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3007 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1705  wcel 1992  wral 2912  wrex 2913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-12 2049
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-nf 1707  df-ral 2917  df-rex 2918
This theorem is referenced by:  tz7.49  7486  hsmexlem2  9194  acunirnmpt2  29293  acunirnmpt2f  29294  locfinreflem  29681  cmpcref  29691  indexdom  33147  filbcmb  33153  cdlemefr29exN  35156  rexanuz3  38746  disjrnmpt2  38835  fompt  38839  disjinfi  38840  iunmapsn  38869  infnsuprnmpt  38928  rnmptbdlem  38933  supxrge  39005  suplesup  39006  infxr  39034  allbutfi  39067  supxrunb3  39074  infxrunb3rnmpt  39106  limsupre  39264  limsupub  39327  limsupre3lem  39355  stoweidlem31  39542  stoweidlem34  39545  fourierdlem73  39690  sge0pnffigt  39907  sge0ltfirp  39911  sge0reuzb  39959  iundjiun  39971  ovnlerp  40070  smflimlem4  40276  smflimsuplem7  40326  2reurex  40472
  Copyright terms: Public domain W3C validator