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

Theorem reximi2 2804
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 1585 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2703 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2703 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43imtr4i 258 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1550    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  pssnn  7318  btwnz  10361  xrsupexmnf  10872  xrinfmexpnf  10873  xrsupsslem  10874  xrinfmsslem  10875  supxrun  10883  ioo0  10930  resqrex  12044  resqreu  12046  rexuzre  12144  neiptopnei  17184  filssufilg  17931  alexsubALTlem4  18069  lgsquadlem2  21127  nmobndseqi  22268  nmobndseqiOLD  22269  pjnmopi  23639  dya2iocuni  24621  ballotlemfc0  24738  ballotlemfcc  24739  ballotlemsup  24750  comppfsc  26324  sstotbnd3  26422  aaitgo  27282  stoweidlem14  27677  stoweidlem57  27720  lsateln0  29632  pclcmpatN  30537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-rex 2703
  Copyright terms: Public domain W3C validator