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

Theorem vtoclga 2815
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 2329 . 2 𝑥𝐴
2 nfv 1538 . 2 𝑥𝜓
3 vtoclga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclga.2 . 2 (𝑥𝐵𝜑)
51, 2, 3, 4vtoclgaf 2814 1 (𝐴𝐵𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105   = wceq 1363  wcel 2158
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751
This theorem is referenced by:  vtoclri  2824  ssuni  3843  ordtriexmid  4532  onsucsssucexmid  4538  tfis3  4597  fvmpt3  5608  fvmptssdm  5613  fnressn  5715  fressnfv  5716  caovord  6060  caovimo  6082  tfrlem1  6323  nnacl  6495  nnmcl  6496  nnacom  6499  nnaass  6500  nndi  6501  nnmass  6502  nnmsucr  6503  nnmcom  6504  nnsucsssuc  6507  nntri3or  6508  nnaordi  6523  nnaword  6526  nnmordi  6531  nnaordex  6543  ixpfn  6718  findcard  6902  findcard2  6903  findcard2s  6904  exmidomni  7154  indpi  7355  prarloclem3  7510  uzind4s2  9605  cnref1o  9664  frec2uzrdg  10423  expcl2lemap  10546  seq3coll  10836  climub  11366  climserle  11367  fsum3cvg  11400  summodclem2a  11403  prodfap0  11567  prodfrecap  11568  fproddccvg  11594  alginv  12061  algcvg  12062  algcvga  12065  algfx  12066  prmind2  12134  prmpwdvds  12367  lgsdir2lem4  14785
  Copyright terms: Public domain W3C validator