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

Theorem reximdai 3041
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 2986 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
4 rexim 3037 . 2 (∀𝑥𝐴 (𝜓𝜒) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
53, 4syl 17 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1748  wcel 2030  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946  df-rex 2947
This theorem is referenced by:  tz7.49  7585  hsmexlem2  9287  acunirnmpt2  29588  acunirnmpt2f  29589  locfinreflem  30035  cmpcref  30045  indexdom  33659  filbcmb  33665  cdlemefr29exN  36007  rexanuz3  39589  reximdd  39658  disjrnmpt2  39689  fompt  39693  disjinfi  39694  iunmapsn  39723  infnsuprnmpt  39779  rnmptbdlem  39784  supxrge  39867  suplesup  39868  infxr  39896  allbutfi  39929  supxrunb3  39936  infxrunb3rnmpt  39968  infrpgernmpt  40008  limsupre  40191  limsupub  40254  limsupre3lem  40282  limsupgtlem  40327  xlimmnfvlem1  40376  xlimpnfvlem1  40380  stoweidlem31  40566  stoweidlem34  40569  fourierdlem73  40714  sge0pnffigt  40931  sge0ltfirp  40935  sge0reuzb  40983  iundjiun  40995  ovnlerp  41097  smflimlem4  41303  smflimsuplem7  41353  2reurex  41502
  Copyright terms: Public domain W3C validator