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

Theorem reximi2 3039
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 1802 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2947 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2947 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 281 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1744  wcel 2030  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
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-rex 2947
This theorem is referenced by:  pssnn  8219  btwnz  11517  xrsupexmnf  12173  xrinfmexpnf  12174  xrsupsslem  12175  xrinfmsslem  12176  supxrun  12184  ioo0  12238  resqrex  14035  resqreu  14037  rexuzre  14136  neiptopnei  20984  comppfsc  21383  filssufilg  21762  alexsubALTlem4  21901  lgsquadlem2  25151  nmobndseqi  27762  nmobndseqiALT  27763  pjnmopi  29135  crefdf  30043  dya2iocuni  30473  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsup  30694  poimirlem32  33571  sstotbnd3  33705  lsateln0  34600  pclcmpatN  35505  aaitgo  38049  stoweidlem14  40549  stoweidlem57  40592  elaa2  40769
  Copyright terms: Public domain W3C validator