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

Theorem reximi2 3079
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 1835 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3072 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3072 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 293 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1779  wcel 2104  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 206  df-ex 1780  df-rex 3072
This theorem is referenced by:  reximia  3081  pssnn  8985  pssnnOLD  9080  btwnz  12465  xrsupexmnf  13081  xrinfmexpnf  13082  xrsupsslem  13083  xrinfmsslem  13084  supxrun  13092  ioo0  13146  hashgt23el  14180  resqrex  15003  resqreu  15005  rexuzre  15105  neiptopnei  22324  comppfsc  22724  filssufilg  23103  alexsubALTlem4  23242  lgsquadlem2  26570  nmobndseqi  29182  nmobndseqiALT  29183  pjnmopi  30551  crefdf  31839  dya2iocuni  32291  ballotlemfc0  32500  ballotlemfcc  32501  ballotlemsup  32512  fnrelpredd  33102  poimirlem32  35850  sstotbnd3  35975  lsateln0  37048  pclcmpatN  37954  aaitgo  41024  stoweidlem14  43603  stoweidlem57  43646  elaa2  43823
  Copyright terms: Public domain W3C validator