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

Theorem vtocl 2714
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.)
Hypotheses
Ref Expression
vtocl.1 𝐴 ∈ V
vtocl.2 (𝑥 = 𝐴 → (𝜑𝜓))
vtocl.3 𝜑
Assertion
Ref Expression
vtocl 𝜓
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem vtocl
StepHypRef Expression
1 nfv 1493 . 2 𝑥𝜓
2 vtocl.1 . 2 𝐴 ∈ V
3 vtocl.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtocl.3 . 2 𝜑
51, 2, 3, 4vtoclf 2713 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316  wcel 1465  Vcvv 2660
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  vtoclb  2717  zfauscl  4018  bnd2  4067  uniex  4329  ordtriexmid  4407  onsucsssucexmid  4412  regexmid  4420  ordsoexmid  4447  onintexmid  4457  reg3exmid  4464  nnregexmid  4504  acexmidlemv  5740  caovcan  5903  findcard2  6751  findcard2s  6752  inffiexmid  6768  sup3exmid  8683  bj-uniex  13042  bj-omtrans  13081
  Copyright terms: Public domain W3C validator