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

Theorem reximi2 2931
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 1635 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2820 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2820 . 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 1596    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-rex 2820
This theorem is referenced by:  pssnn  7735  btwnz  10959  xrsupexmnf  11492  xrinfmexpnf  11493  xrsupsslem  11494  xrinfmsslem  11495  supxrun  11503  ioo0  11550  resqrex  13043  resqreu  13045  rexuzre  13144  neiptopnei  19399  filssufilg  20147  alexsubALTlem4  20285  lgsquadlem2  23358  nmobndseqi  25370  nmobndseqiOLD  25371  pjnmopi  26743  dya2iocuni  27894  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemsup  28083  comppfsc  29779  sstotbnd3  29875  aaitgo  30716  stoweidlem14  31314  stoweidlem57  31357  lsateln0  33792  pclcmpatN  34697
  Copyright terms: Public domain W3C validator