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

Theorem rspcdv 3055
 Description: Restricted specialization, using implicit substitution. (Contributed by NM, 17-Feb-2007.) (Revised by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
rspcdv.1
rspcdv.2
Assertion
Ref Expression
rspcdv
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem rspcdv
StepHypRef Expression
1 rspcdv.1 . 2
2 rspcdv.2 . . 3
32biimpd 199 . 2
41, 3rspcimdv 3053 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  wral 2705 This theorem is referenced by:  ralxfrd  4737  zindd  10371  ismri2dad  13862  mreexd  13867  mreexexlemd  13869  catcocl  13910  catass  13911  moni  13962  subccocl  14042  funcco  14068  fullfo  14109  fthf1  14114  nati  14152  sizeusglecusglem1  21493  fargshiftfva  21626  eupatrl  21690  esumcvg  24476  orvcelel  24727  onint1  26199  ralbinrald  27953  ralxfrd2  28072  cshwsame  28277  usg2wlkeq  28304 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958
 Copyright terms: Public domain W3C validator