ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  vtoclga Structured version   GIF version

Theorem vtoclga 2590
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1 (x = A → (φψ))
vtoclga.2 (x Bφ)
Assertion
Ref Expression
vtoclga (A Bψ)
Distinct variable groups:   x,A   x,B   ψ,x
Allowed substitution hint:   φ(x)

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2154 . 2 xA
2 nfv 1397 . 2 xψ
3 vtoclga.1 . 2 (x = A → (φψ))
4 vtoclga.2 . 2 (x Bφ)
51, 2, 3, 4vtoclgaf 2589 1 (A Bψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   = wceq 1226   wcel 1369
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1622  df-clab 2003  df-cleq 2009  df-clel 2012  df-nfc 2143  df-v 2531
This theorem is referenced by:  vtoclri  2599  ssuni  3568  ordtriexmid  4185  onsucsssucexmid  4187  tfis3  4227  fvmpt3  5167  fvmptssdm  5171  fnressn  5265  fressnfv  5266  caovord  5586  caovimo  5608  tfrlem1  5836  tfrlemi14  5860  nnacl  5965  nnmcl  5966  nnacom  5969  nnaass  5970  nndi  5971  nnmass  5972  nnmsucr  5973  nnmcom  5974  nnsucsssuc  5977  nntri3or  5978  nnaordi  5983  nnaword  5986  nnmordi  5991  nnaordex  6002  prarloclem3  6340
  Copyright terms: Public domain W3C validator