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

Theorem reximi2 2988
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 1750 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2897 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2897 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 279 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694  wcel 1975  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726
This theorem depends on definitions:  df-bi 195  df-ex 1695  df-rex 2897
This theorem is referenced by:  pssnn  8036  btwnz  11307  xrsupexmnf  11959  xrinfmexpnf  11960  xrsupsslem  11961  xrinfmsslem  11962  supxrun  11970  ioo0  12023  resqrex  13781  resqreu  13783  rexuzre  13882  neiptopnei  20684  comppfsc  21083  filssufilg  21463  alexsubALTlem4  21602  lgsquadlem2  24819  nmobndseqi  26820  nmobndseqiALT  26821  pjnmopi  28193  crefdf  29045  dya2iocuni  29474  ballotlemfc0  29683  ballotlemfcc  29684  ballotlemsup  29695  poimirlem32  32410  sstotbnd3  32544  lsateln0  33099  pclcmpatN  34004  aaitgo  36550  stoweidlem14  38707  stoweidlem57  38750  elaa2  38927
  Copyright terms: Public domain W3C validator