Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  vtocl Unicode version

Theorem vtocl 2654
 Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
Hypotheses
Ref Expression
vtocl.1
vtocl.2
vtocl.3
Assertion
Ref Expression
vtocl
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem vtocl
StepHypRef Expression
1 nfv 1462 . 2
2 vtocl.1 . 2
3 vtocl.2 . 2
4 vtocl.3 . 2
51, 2, 3, 4vtoclf 2653 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 103   wceq 1285   wcel 1434  cvv 2602 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604 This theorem is referenced by:  vtoclb  2657  zfauscl  3906  bnd2  3955  pwex  3961  uniex  4200  ordtriexmid  4273  onsucsssucexmid  4278  regexmid  4286  ordsoexmid  4313  onintexmid  4323  reg3exmid  4330  nnregexmid  4368  acexmidlemv  5541  caovcan  5696  findcard2  6423  findcard2s  6424  bj-uniex  10866  bj-omtrans  10909
 Copyright terms: Public domain W3C validator