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

Theorem reximi2 3207
 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 1836 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3112 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3112 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 295 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-rex 3112 This theorem is referenced by:  pssnn  8722  btwnz  12074  xrsupexmnf  12688  xrinfmexpnf  12689  xrsupsslem  12690  xrinfmsslem  12691  supxrun  12699  ioo0  12753  hashgt23el  13783  resqrex  14604  resqreu  14606  rexuzre  14706  neiptopnei  21744  comppfsc  22144  filssufilg  22523  alexsubALTlem4  22662  lgsquadlem2  25972  nmobndseqi  28569  nmobndseqiALT  28570  pjnmopi  29938  crefdf  31213  dya2iocuni  31663  ballotlemfc0  31872  ballotlemfcc  31873  ballotlemsup  31884  fnrelpredd  32484  poimirlem32  35105  sstotbnd3  35230  lsateln0  36307  pclcmpatN  37213  aaitgo  40121  stoweidlem14  42671  stoweidlem57  42714  elaa2  42891
 Copyright terms: Public domain W3C validator