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

Theorem reximi2 3241
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 1826 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3141 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3141 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 293 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1771  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-rex 3141
This theorem is referenced by:  pssnn  8724  btwnz  12072  xrsupexmnf  12686  xrinfmexpnf  12687  xrsupsslem  12688  xrinfmsslem  12689  supxrun  12697  ioo0  12751  hashgt23el  13773  resqrex  14598  resqreu  14600  rexuzre  14700  neiptopnei  21668  comppfsc  22068  filssufilg  22447  alexsubALTlem4  22586  lgsquadlem2  25884  nmobndseqi  28483  nmobndseqiALT  28484  pjnmopi  29852  crefdf  31011  dya2iocuni  31440  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemsup  31661  poimirlem32  34805  sstotbnd3  34935  lsateln0  36011  pclcmpatN  36917  aaitgo  39640  stoweidlem14  42176  stoweidlem57  42219  elaa2  42396
  Copyright terms: Public domain W3C validator