![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > vtocl | Structured version Unicode version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
vtocl.1 |
![]() ![]() ![]() ![]() |
vtocl.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtocl.3 |
![]() ![]() |
Ref | Expression |
---|---|
vtocl |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1674 |
. 2
![]() ![]() ![]() ![]() | |
2 | vtocl.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | vtocl.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | vtocl.3 |
. 2
![]() ![]() | |
5 | 1, 2, 3, 4 | vtoclf 3129 |
1
![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-12 1794 ax-ext 2432 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2440 df-cleq 2446 df-clel 2449 df-v 3080 |
This theorem is referenced by: vtoclb 3133 zfauscl 4526 pwex 4586 fnbrfvb 5844 caovcan 6380 uniex 6489 findcard2 7666 zfregcl 7923 bnd2 8214 kmlem2 8434 axcc2lem 8719 dominf 8728 dcomex 8730 ac4c 8759 ac5 8760 dominfac 8851 pwfseqlem4 8943 grothomex 9110 ramub2 14196 ismred2 14663 dvfsumlem2 21635 plydivlem4 21898 frmin 27867 voliunnfl 28603 volsupnfl 28604 prdsbnd2 28862 iscringd 28967 monotoddzzfi 29451 monotoddzz 29452 bnj865 32268 bnj1015 32306 |
Copyright terms: Public domain | W3C validator |