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

Theorem vtoclg 2659
Description: Implicit substitution of a class expression for a setvar variable. (Contributed by NM, 17-Apr-1995.)
Hypotheses
Ref Expression
vtoclg.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtoclg.2  |-  ph
Assertion
Ref Expression
vtoclg  |-  ( A  e.  V  ->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem vtoclg
StepHypRef Expression
1 nfcv 2220 . 2  |-  F/_ x A
2 nfv 1462 . 2  |-  F/ x ps
3 vtoclg.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
4 vtoclg.2 . 2  |-  ph
51, 2, 3, 4vtoclgf 2658 1  |-  ( A  e.  V  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1285    e. wcel 1434
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604
This theorem is referenced by:  vtoclbg  2660  ceqex  2723  mo2icl  2772  nelrdva  2798  sbctt  2881  sbcnestgf  2954  csbing  3180  prnzg  3522  sneqrg  3562  unisng  3626  csbopabg  3864  trss  3892  inex1g  3922  ssexg  3925  pwexg  3962  prexg  3974  opth  4000  ordelord  4144  uniexg  4201  vtoclr  4414  resieq  4650  csbima12g  4716  dmsnsnsng  4828  iota5  4917  csbiotag  4925  funmo  4947  fconstg  5114  funfveu  5219  funbrfv  5244  fnbrfvb  5246  fvelimab  5261  ssimaexg  5267  fvelrn  5330  isoselem  5490  csbriotag  5511  csbov123g  5574  ovg  5670  tfrexlem  5983  rdg0g  6037  ensn1g  6344  fundmeng  6354  xpdom2g  6376  phplem3g  6391  prcdnql  6736  prcunqu  6737  prdisj  6744  shftvalg  9862  shftval4g  9863  climshft  10281  lcmgcdlem  10603  bdzfauscl  10839  bdinex1g  10850  bdssexg  10853  bj-prexg  10860  bj-uniexg  10867
  Copyright terms: Public domain W3C validator