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

Theorem reximi2 3171
Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)
Hypothesis
Ref Expression
reximi2.1 ((𝑥𝐴𝜑) → (𝑥𝐵𝜓))
Assertion
Ref Expression
reximi2 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)

Proof of Theorem reximi2
StepHypRef Expression
1 reximi2.1 . . 3 ((𝑥𝐴𝜑) → (𝑥𝐵𝜓))
21eximi 1838 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3069 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3069 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 291 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1783  wcel 2108  wrex 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813
This theorem depends on definitions:  df-bi 206  df-ex 1784  df-rex 3069
This theorem is referenced by:  reximia  3172  pssnn  8913  pssnnOLD  8969  btwnz  12352  xrsupexmnf  12968  xrinfmexpnf  12969  xrsupsslem  12970  xrinfmsslem  12971  supxrun  12979  ioo0  13033  hashgt23el  14067  resqrex  14890  resqreu  14892  rexuzre  14992  neiptopnei  22191  comppfsc  22591  filssufilg  22970  alexsubALTlem4  23109  lgsquadlem2  26434  nmobndseqi  29042  nmobndseqiALT  29043  pjnmopi  30411  crefdf  31700  dya2iocuni  32150  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsup  32371  fnrelpredd  32961  poimirlem32  35736  sstotbnd3  35861  lsateln0  36936  pclcmpatN  37842  aaitgo  40903  stoweidlem14  43445  stoweidlem57  43488  elaa2  43665
  Copyright terms: Public domain W3C validator