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 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3071 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 292 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1779  wcel 2108  wrex 3070
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 207  df-ex 1780  df-rex 3071
This theorem is referenced by:  reximia  3081  pssnn  9208  btwnz  12721  xrsupexmnf  13347  xrinfmexpnf  13348  xrsupsslem  13349  xrinfmsslem  13350  supxrun  13358  ioo0  13412  hashgt23el  14463  resqrex  15289  resqreu  15291  rexuzre  15391  neiptopnei  23140  comppfsc  23540  filssufilg  23919  alexsubALTlem4  24058  lgsquadlem2  27425  nmobndseqi  30798  nmobndseqiALT  30799  pjnmopi  32167  crefdf  33847  dya2iocuni  34285  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsup  34507  fnrelpredd  35103  poimirlem32  37659  sstotbnd3  37783  lsateln0  38996  pclcmpatN  39903  aaitgo  43174  stoweidlem14  46029  stoweidlem57  46072  elaa2  46249
  Copyright terms: Public domain W3C validator