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

Theorem reximi2 2622
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 1574 . 2  |-  ( E. x ( x  e.  A  /\  ph )  ->  E. x ( x  e.  B  /\  ps ) )
3 df-rex 2522 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
4 df-rex 2522 . 2  |-  ( E. x  e.  B  ps  <->  E. x ( x  e.  B  /\  ps )
)
52, 3, 43imtr4i 259 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360   E.wex 1537    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  pssnn  7035  btwnz  10067  xrsupexmnf  10575  xrinfmexpnf  10576  xrsupsslem  10577  xrinfmsslem  10578  supxrun  10586  ioo0  10633  resqrex  11687  resqreu  11689  rexuzre  11787  filssufilg  17554  alexsubALTlem4  17692  lgsquadlem2  20542  nmobndseqi  21303  nmobndseqiOLD  21304  pjnmopi  22674  ballotlemfc0  22998  ballotlemfcc  22999  ballotlemsup  23010  comppfsc  25660  sstotbnd3  25853  aaitgo  26720  lsateln0  28336  pclcmpatN  29241
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-rex 2522
  Copyright terms: Public domain W3C validator