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

Theorem reximi2 3185
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 1797 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3088 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3088 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 284 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  wex 1742  wcel 2048  wrex 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772
This theorem depends on definitions:  df-bi 199  df-ex 1743  df-rex 3088
This theorem is referenced by:  pssnn  8523  btwnz  11890  xrsupexmnf  12507  xrinfmexpnf  12508  xrsupsslem  12509  xrinfmsslem  12510  supxrun  12518  ioo0  12572  resqrex  14461  resqreu  14463  rexuzre  14563  neiptopnei  21434  comppfsc  21834  filssufilg  22213  alexsubALTlem4  22352  lgsquadlem2  25649  nmobndseqi  28323  nmobndseqiALT  28324  pjnmopi  29696  crefdf  30713  dya2iocuni  31143  ballotlemfc0  31353  ballotlemfcc  31354  ballotlemsup  31365  poimirlem32  34313  sstotbnd3  34444  lsateln0  35524  pclcmpatN  36430  aaitgo  39103  stoweidlem14  41676  stoweidlem57  41719  elaa2  41896
  Copyright terms: Public domain W3C validator