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

Theorem reximi2 3007
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 1760 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥(𝑥𝐵𝜓))
3 df-rex 2915 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
4 df-rex 2915 . 2 (∃𝑥𝐵 𝜓 ↔ ∃𝑥(𝑥𝐵𝜓))
52, 3, 43imtr4i 281 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wex 1702  wcel 1988  wrex 2910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ex 1703  df-rex 2915
This theorem is referenced by:  pssnn  8163  btwnz  11464  xrsupexmnf  12120  xrinfmexpnf  12121  xrsupsslem  12122  xrinfmsslem  12123  supxrun  12131  ioo0  12185  resqrex  13972  resqreu  13974  rexuzre  14073  neiptopnei  20917  comppfsc  21316  filssufilg  21696  alexsubALTlem4  21835  lgsquadlem2  25087  nmobndseqi  27604  nmobndseqiALT  27605  pjnmopi  28977  crefdf  29889  dya2iocuni  30319  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemsup  30540  poimirlem32  33412  sstotbnd3  33546  lsateln0  34101  pclcmpatN  35006  aaitgo  37551  stoweidlem14  39994  stoweidlem57  40037  elaa2  40214
  Copyright terms: Public domain W3C validator