Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclgaf Structured version   Unicode version

Theorem vtoclgaf 3016
 Description: Implicit substitution of a class for a set variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.)
Hypotheses
Ref Expression
vtoclgaf.1
vtoclgaf.2
vtoclgaf.3
vtoclgaf.4
Assertion
Ref Expression
vtoclgaf
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem vtoclgaf
StepHypRef Expression
1 vtoclgaf.1 . . 3
21nfel1 2582 . . . 4
3 vtoclgaf.2 . . . 4
42, 3nfim 1832 . . 3
5 eleq1 2496 . . . 4
6 vtoclgaf.3 . . . 4
75, 6imbi12d 312 . . 3
8 vtoclgaf.4 . . 3
91, 4, 7, 8vtoclgf 3010 . 2
109pm2.43i 45 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177  wnf 1553   wceq 1652   wcel 1725  wnfc 2559 This theorem is referenced by:  vtoclga  3017  ssiun2s  4135  tfis  4834  fvmptss  5813  fvmptf  5821  fmptco  5901  inar1  8650  sumss  12518  prmind2  13090  lss1d  16039  itg2splitlem  19640  dgrle  20162  cnlnadjlem5  23574  fprodn0  25303  stoweidlem26  27751 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958
 Copyright terms: Public domain W3C validator