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

Theorem vtoclg 2718
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 2256 . 2 𝑥𝐴
2 nfv 1491 . 2 𝑥𝜓
3 vtoclg.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclg.2 . 2 𝜑
51, 2, 3, 4vtoclgf 2716 1 (𝐴𝑉𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wcel 1463
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660
This theorem is referenced by:  vtoclbg  2719  ceqex  2784  mo2icl  2834  nelrdva  2862  sbctt  2945  sbcnestgf  3019  csbing  3251  ifmdc  3477  prnzg  3615  sneqrg  3657  unisng  3721  csbopabg  3974  trss  4003  inex1g  4032  ssexg  4035  pwexg  4072  prexg  4101  opth  4127  ordelord  4271  uniexg  4329  vtoclr  4555  resieq  4797  csbima12g  4868  dmsnsnsng  4984  iota5  5076  csbiotag  5084  funmo  5106  fconstg  5287  funfveu  5400  funbrfv  5426  fnbrfvb  5428  fvelimab  5443  ssimaexg  5449  fvelrn  5517  isoselem  5687  csbriotag  5708  csbov123g  5775  ovg  5875  tfrexlem  6197  rdg0g  6251  ensn1g  6657  fundmeng  6667  xpdom2g  6692  phplem3g  6716  prcdnql  7256  prcunqu  7257  prdisj  7264  shftvalg  10548  shftval4g  10549  climshft  11013  telfsumo  11175  fsumparts  11179  lcmgcdlem  11654  fiinopn  12066  bdzfauscl  12911  bdinex1g  12922  bdssexg  12925  bj-prexg  12932  bj-uniexg  12939
  Copyright terms: Public domain W3C validator