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

Theorem reximi2 2649
 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
Assertion
Ref Expression
reximi2

Proof of Theorem reximi2
StepHypRef Expression
1 reximi2.1 . . 3
21eximi 1563 . 2
3 df-rex 2549 . 2
4 df-rex 2549 . 2
52, 3, 43imtr4i 257 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358  wex 1528   wcel 1684  wrex 2544 This theorem is referenced by:  pssnn  7081  btwnz  10114  xrsupexmnf  10623  xrinfmexpnf  10624  xrsupsslem  10625  xrinfmsslem  10626  supxrun  10634  ioo0  10681  resqrex  11736  resqreu  11738  rexuzre  11836  filssufilg  17606  alexsubALTlem4  17744  lgsquadlem2  20594  nmobndseqi  21357  nmobndseqiOLD  21358  pjnmopi  22728  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemsup  23063  comppfsc  26307  sstotbnd3  26500  aaitgo  27367  lsateln0  29185  pclcmpatN  30090 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544 This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
 Copyright terms: Public domain W3C validator