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

Theorem vtoclg 2682
Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
Hypotheses
Ref Expression
vtoclg.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclg.2 𝜑
Assertion
Ref Expression
vtoclg (𝐴𝑉𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclg
StepHypRef Expression
1 nfcv 2229 . 2 𝑥𝐴
2 nfv 1467 . 2 𝑥𝜓
3 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclg.2 . 2 𝜑
51, 2, 3, 4vtoclgf 2680 1 (𝐴𝑉𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1290  wcel 1439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2624
This theorem is referenced by:  vtoclbg  2683  ceqex  2747  mo2icl  2797  nelrdva  2825  sbctt  2908  sbcnestgf  2982  csbing  3210  ifmdc  3434  prnzg  3572  sneqrg  3614  unisng  3678  csbopabg  3924  trss  3953  inex1g  3983  ssexg  3986  pwexg  4023  prexg  4049  opth  4075  ordelord  4219  uniexg  4277  vtoclr  4501  resieq  4738  csbima12g  4808  dmsnsnsng  4923  iota5  5015  csbiotag  5023  funmo  5045  fconstg  5222  funfveu  5333  funbrfv  5358  fnbrfvb  5360  fvelimab  5375  ssimaexg  5381  fvelrn  5446  isoselem  5615  csbriotag  5636  csbov123g  5703  ovg  5799  tfrexlem  6115  rdg0g  6169  ensn1g  6570  fundmeng  6580  xpdom2g  6604  phplem3g  6628  prcdnql  7106  prcunqu  7107  prdisj  7114  shftvalg  10333  shftval4g  10334  climshft  10755  telfsumo  10923  fsumparts  10927  lcmgcdlem  11400  fiinopn  11766  bdzfauscl  12085  bdinex1g  12096  bdssexg  12099  bj-prexg  12106  bj-uniexg  12113
  Copyright terms: Public domain W3C validator