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

Theorem reximi2 2812
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 1626 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2711 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2711 . 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 1589    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-rex 2711
This theorem is referenced by:  pssnn  7519  btwnz  10732  xrsupexmnf  11255  xrinfmexpnf  11256  xrsupsslem  11257  xrinfmsslem  11258  supxrun  11266  ioo0  11313  resqrex  12724  resqreu  12726  rexuzre  12824  neiptopnei  18578  filssufilg  19326  alexsubALTlem4  19464  lgsquadlem2  22579  nmobndseqi  24002  nmobndseqiOLD  24003  pjnmopi  25375  dya2iocuni  26552  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemsup  26735  comppfsc  28423  sstotbnd3  28519  aaitgo  29364  stoweidlem14  29655  stoweidlem57  29698  lsateln0  32234  pclcmpatN  33139
  Copyright terms: Public domain W3C validator