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

Theorem vtoclg 2720
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 2258 . 2 𝑥𝐴
2 nfv 1493 . 2 𝑥𝜓
3 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclg.2 . 2 𝜑
51, 2, 3, 4vtoclgf 2718 1 (𝐴𝑉𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316  wcel 1465
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662
This theorem is referenced by:  vtoclbg  2721  ceqex  2786  mo2icl  2836  nelrdva  2864  sbctt  2947  sbcnestgf  3021  csbing  3253  ifmdc  3479  prnzg  3617  sneqrg  3659  unisng  3723  csbopabg  3976  trss  4005  inex1g  4034  ssexg  4037  pwexg  4074  prexg  4103  opth  4129  ordelord  4273  uniexg  4331  vtoclr  4557  resieq  4799  csbima12g  4870  dmsnsnsng  4986  iota5  5078  csbiotag  5086  funmo  5108  fconstg  5289  funfveu  5402  funbrfv  5428  fnbrfvb  5430  fvelimab  5445  ssimaexg  5451  fvelrn  5519  isoselem  5689  csbriotag  5710  csbov123g  5777  ovg  5877  tfrexlem  6199  rdg0g  6253  ensn1g  6659  fundmeng  6669  xpdom2g  6694  phplem3g  6718  prcdnql  7260  prcunqu  7261  prdisj  7268  shftvalg  10563  shftval4g  10564  climshft  11028  telfsumo  11190  fsumparts  11194  lcmgcdlem  11670  fiinopn  12082  bdzfauscl  12984  bdinex1g  12995  bdssexg  12998  bj-prexg  13005  bj-uniexg  13012
  Copyright terms: Public domain W3C validator