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

Theorem reximi2 2620
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 1574 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2521 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2521 . 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 1537    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  pssnn  7014  btwnz  10046  xrsupexmnf  10554  xrinfmexpnf  10555  xrsupsslem  10556  xrinfmsslem  10557  supxrun  10565  ioo0  10612  resqrex  11666  resqreu  11668  rexuzre  11766  filssufilg  17533  alexsubALTlem4  17671  lgsquadlem2  20521  nmobndseqi  21282  nmobndseqiOLD  21283  pjnmopi  22653  ballotlemfc0  22977  ballotlemfcc  22978  ballotlemsup  22989  comppfsc  25639  sstotbnd3  25832  aaitgo  26699  lsateln0  28315  pclcmpatN  29220
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-rex 2521
  Copyright terms: Public domain W3C validator