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

Theorem reximi2 2662
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 1566 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2562 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2562 . 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 1531    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  pssnn  7097  btwnz  10130  xrsupexmnf  10639  xrinfmexpnf  10640  xrsupsslem  10641  xrinfmsslem  10642  supxrun  10650  ioo0  10697  resqrex  11752  resqreu  11754  rexuzre  11852  filssufilg  17622  alexsubALTlem4  17760  lgsquadlem2  20610  nmobndseqi  21373  nmobndseqiOLD  21374  pjnmopi  22744  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemsup  23079  comppfsc  26410  sstotbnd3  26603  aaitgo  27470  lsateln0  29807  pclcmpatN  30712
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-rex 2562
  Copyright terms: Public domain W3C validator