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

Theorem vtocl 2687
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 1473 . 2 𝑥𝜓
2 vtocl.1 . 2 𝐴 ∈ V
3 vtocl.2 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
4 vtocl.3 . 2 𝜑
51, 2, 3, 4vtoclf 2686 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1296  wcel 1445  Vcvv 2633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-v 2635
This theorem is referenced by:  vtoclb  2690  zfauscl  3980  bnd2  4029  uniex  4288  ordtriexmid  4366  onsucsssucexmid  4371  regexmid  4379  ordsoexmid  4406  onintexmid  4416  reg3exmid  4423  nnregexmid  4462  acexmidlemv  5688  caovcan  5847  findcard2  6685  findcard2s  6686  inffiexmid  6702  sup3exmid  8515  bj-uniex  12532  bj-omtrans  12575
  Copyright terms: Public domain W3C validator