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

Theorem reximi2 2825
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  |-  ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ps )
)
Assertion
Ref Expression
reximi2  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )

Proof of Theorem reximi2
StepHypRef Expression
1 reximi2.1 . . 3  |-  ( ( x  e.  A  /\  ph )  ->  ( x  e.  B  /\  ps )
)
21eximi 1625 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2724 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2724 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43imtr4i 266 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586    e. wcel 1756   E.wrex 2719
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-rex 2724
This theorem is referenced by:  pssnn  7534  btwnz  10747  xrsupexmnf  11270  xrinfmexpnf  11271  xrsupsslem  11272  xrinfmsslem  11273  supxrun  11281  ioo0  11328  resqrex  12743  resqreu  12745  rexuzre  12843  neiptopnei  18739  filssufilg  19487  alexsubALTlem4  19625  lgsquadlem2  22697  nmobndseqi  24182  nmobndseqiOLD  24183  pjnmopi  25555  dya2iocuni  26701  ballotlemfc0  26878  ballotlemfcc  26879  ballotlemsup  26890  comppfsc  28582  sstotbnd3  28678  aaitgo  29522  stoweidlem14  29812  stoweidlem57  29855  lsateln0  32643  pclcmpatN  33548
  Copyright terms: Public domain W3C validator