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

Theorem vtoclga 2678
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtoclga.1 (𝑥 = 𝐴 → (𝜑𝜓))
vtoclga.2 (𝑥𝐵𝜑)
Assertion
Ref Expression
vtoclga (𝐴𝐵𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtoclga
StepHypRef Expression
1 nfcv 2225 . 2 𝑥𝐴
2 nfv 1464 . 2 𝑥𝜓
3 vtoclga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclga.2 . 2 (𝑥𝐵𝜑)
51, 2, 3, 4vtoclgaf 2677 1 (𝐴𝐵𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287  wcel 1436
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-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617
This theorem is referenced by:  vtoclri  2687  ssuni  3658  ordtriexmid  4311  onsucsssucexmid  4316  tfis3  4374  fvmpt3  5346  fvmptssdm  5350  fnressn  5446  fressnfv  5447  caovord  5773  caovimo  5795  tfrlem1  6027  nnacl  6195  nnmcl  6196  nnacom  6199  nnaass  6200  nndi  6201  nnmass  6202  nnmsucr  6203  nnmcom  6204  nnsucsssuc  6207  nntri3or  6208  nnaordi  6219  nnaword  6222  nnmordi  6227  nnaordex  6238  findcard  6556  findcard2  6557  findcard2s  6558  exmidomni  6742  indpi  6845  prarloclem3  7000  uzind4s2  9011  cnref1o  9065  frec2uzrdg  9744  expcl2lemap  9865  iseqcoll  10143  climub  10624  climserile  10625  fisumcvg  10656  isummolem2a  10660  ialginv  10904  ialgcvg  10905  ialgcvga  10908  ialgfx  10909  prmind2  10977
  Copyright terms: Public domain W3C validator