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

Theorem vtoclga 2726
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 2258 . 2 𝑥𝐴
2 nfv 1493 . 2 𝑥𝜓
3 vtoclga.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtoclga.2 . 2 (𝑥𝐵𝜑)
51, 2, 3, 4vtoclgaf 2725 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:  vtoclri  2735  ssuni  3728  ordtriexmid  4407  onsucsssucexmid  4412  tfis3  4470  fvmpt3  5468  fvmptssdm  5473  fnressn  5574  fressnfv  5575  caovord  5910  caovimo  5932  tfrlem1  6173  nnacl  6344  nnmcl  6345  nnacom  6348  nnaass  6349  nndi  6350  nnmass  6351  nnmsucr  6352  nnmcom  6353  nnsucsssuc  6356  nntri3or  6357  nnaordi  6372  nnaword  6375  nnmordi  6380  nnaordex  6391  ixpfn  6566  findcard  6750  findcard2  6751  findcard2s  6752  exmidomni  6982  indpi  7118  prarloclem3  7273  uzind4s2  9354  cnref1o  9408  frec2uzrdg  10150  expcl2lemap  10273  seq3coll  10553  climub  11081  climserle  11082  fsum3cvg  11114  summodclem2a  11118  alginv  11655  algcvg  11656  algcvga  11659  algfx  11660  prmind2  11728
  Copyright terms: Public domain W3C validator