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

Theorem reximi2 2650
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 1568 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2550 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2550 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43imtr4i 259 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1533    e. wcel 1688   E.wrex 2545
This theorem is referenced by:  pssnn  7076  btwnz  10109  xrsupexmnf  10617  xrinfmexpnf  10618  xrsupsslem  10619  xrinfmsslem  10620  supxrun  10628  ioo0  10675  resqrex  11730  resqreu  11732  rexuzre  11830  filssufilg  17600  alexsubALTlem4  17738  lgsquadlem2  20588  nmobndseqi  21349  nmobndseqiOLD  21350  pjnmopi  22720  ballotlemfc0  23044  ballotlemfcc  23045  ballotlemsup  23056  comppfsc  25706  sstotbnd3  25899  aaitgo  26766  lsateln0  28452  pclcmpatN  29357
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549
This theorem depends on definitions:  df-bi 179  df-ex 1534  df-rex 2550
  Copyright terms: Public domain W3C validator