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

Theorem reximi2 2921
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 1661 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2810 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2810 . 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 367   E.wex 1617    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-rex 2810
This theorem is referenced by:  pssnn  7731  btwnz  10962  xrsupexmnf  11499  xrinfmexpnf  11500  xrsupsslem  11501  xrinfmsslem  11502  supxrun  11510  ioo0  11557  resqrex  13169  resqreu  13171  rexuzre  13270  neiptopnei  19803  comppfsc  20202  filssufilg  20581  alexsubALTlem4  20719  lgsquadlem2  23831  nmobndseqi  25895  nmobndseqiALT  25896  pjnmopi  27268  crefdf  28089  dya2iocuni  28494  ballotlemfc0  28698  ballotlemfcc  28699  ballotlemsup  28710  sstotbnd3  30515  aaitgo  31355  stoweidlem14  32038  stoweidlem57  32081  elaa2  32259  lsateln0  35136  pclcmpatN  36041
  Copyright terms: Public domain W3C validator