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

Theorem reximi2 3069
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 1830 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 3061 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 3061 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 291 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wex 1774  wcel 2099  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-ex 1775  df-rex 3061
This theorem is referenced by:  reximia  3071  pssnn  9206  pssnnOLD  9299  btwnz  12717  xrsupexmnf  13338  xrinfmexpnf  13339  xrsupsslem  13340  xrinfmsslem  13341  supxrun  13349  ioo0  13403  hashgt23el  14441  resqrex  15255  resqreu  15257  rexuzre  15357  neiptopnei  23127  comppfsc  23527  filssufilg  23906  alexsubALTlem4  24045  lgsquadlem2  27410  nmobndseqi  30712  nmobndseqiALT  30713  pjnmopi  32081  crefdf  33663  dya2iocuni  34117  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemsup  34338  fnrelpredd  34926  poimirlem32  37353  sstotbnd3  37477  lsateln0  38693  pclcmpatN  39600  aaitgo  42823  stoweidlem14  45635  stoweidlem57  45678  elaa2  45855
  Copyright terms: Public domain W3C validator