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

Theorem reximi2 3197
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 1919 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3102 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3102 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 283 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wex 1859  wcel 2156  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-rex 3102
This theorem is referenced by:  pssnn  8413  btwnz  11741  xrsupexmnf  12349  xrinfmexpnf  12350  xrsupsslem  12351  xrinfmsslem  12352  supxrun  12360  ioo0  12414  resqrex  14210  resqreu  14212  rexuzre  14311  neiptopnei  21147  comppfsc  21546  filssufilg  21925  alexsubALTlem4  22064  lgsquadlem2  25319  nmobndseqi  27961  nmobndseqiALT  27962  pjnmopi  29334  crefdf  30239  dya2iocuni  30669  ballotlemfc0  30878  ballotlemfcc  30879  ballotlemsup  30890  poimirlem32  33752  sstotbnd3  33884  lsateln0  34773  pclcmpatN  35679  aaitgo  38230  stoweidlem14  40707  stoweidlem57  40750  elaa2  40927
  Copyright terms: Public domain W3C validator