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

Theorem reximi2 2649
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 1563 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2549 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2549 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43imtr4i 257 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  pssnn  7081  btwnz  10114  xrsupexmnf  10623  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  ioo0  10681  resqrex  11736  resqreu  11738  rexuzre  11836  filssufilg  17606  alexsubALTlem4  17744  lgsquadlem2  20594  nmobndseqi  21357  nmobndseqiOLD  21358  pjnmopi  22728  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsup  23063  comppfsc  26307  sstotbnd3  26500  aaitgo  27367  lsateln0  29185  pclcmpatN  30090
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator