NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  vtocl2g Unicode version

Theorem vtocl2g 2918
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)
Hypotheses
Ref Expression
vtocl2g.1
vtocl2g.2
vtocl2g.3
Assertion
Ref Expression
vtocl2g
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   ()   ()   ()   (,)   (,)

Proof of Theorem vtocl2g
StepHypRef Expression
1 nfcv 2489 . 2  F/_
2 nfcv 2489 . 2  F/_
3 nfcv 2489 . 2  F/_
4 nfv 1619 . 2  F/
5 nfv 1619 . 2  F/
6 vtocl2g.1 . 2
7 vtocl2g.2 . 2
8 vtocl2g.3 . 2
91, 2, 3, 4, 5, 6, 7, 8vtocl2gf 2916 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wa 358   wceq 1642   wcel 1710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861
This theorem is referenced by:  ifexg  3721  uniprg  3906  intprg  3960  ninexg  4097  preqr2g  4126  preaddccan2lem1  4454  spfinsfincl  4539  opelopabsb  4697  br1stg  4730  vtoclr  4816  fnunsn  5190  f1osng  5323  fsng  5433  fvsng  5446  trtxp  5781  oqelins4  5794  qrpprod  5836  clos1exg  5877  clos1conn  5879  clos1basesucg  5884  mapex  6006  xpsneng  6050  xpcomeng  6053  enpw1  6062  enmap2  6068  enpw  6087  addccan2nclem2  6264
  Copyright terms: Public domain W3C validator