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

Theorem r19.29r 2646
 Description: Variation of Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 2645 . 2
2 ancom 439 . 2
3 ancom 439 . . 3
43rexbii 2532 . 2
51, 2, 43imtr4i 259 1
 Colors of variables: wff set class Syntax hints:   wi 6   wa 360  wral 2509  wrex 2510 This theorem is referenced by:  rlimuni  11901  rlimno1  12004  neindisj2  16692  lmss  16858  fclsbas  17548  isfcf  17561  metcnp3  17918  bndth  18288  ellimc3  19061  cmptdst  24734  cover2  25524  bnj517  27606 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-ral 2513  df-rex 2514
 Copyright terms: Public domain W3C validator