Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtocl | Structured version Visualization version Unicode version |
Description: Implicit substitution of a class for a setvar variable. See also vtoclALT 3260. (Contributed by NM, 30-Aug-1993.) Removed dependency on ax-10 2019. (Revised by BJ, 29-Nov-2020.) |
Ref | Expression |
---|---|
vtocl.1 | |
vtocl.2 | |
vtocl.3 |
Ref | Expression |
---|---|
vtocl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocl.1 | . . . . 5 | |
2 | 1 | isseti 3209 | . . . 4 |
3 | vtocl.2 | . . . . 5 | |
4 | 3 | biimpd 219 | . . . 4 |
5 | 2, 4 | eximii 1764 | . . 3 |
6 | 5 | 19.36iv 1905 | . 2 |
7 | vtocl.3 | . 2 | |
8 | 6, 7 | mpg 1724 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wceq 1483 wcel 1990 cvv 3200 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-tru 1486 df-ex 1705 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 |
This theorem is referenced by: vtoclb 3263 zfauscl 4783 pwex 4848 fnbrfvb 6236 caovcan 6838 uniex 6953 findcard2 8200 zfregclOLD 8501 bnd2 8756 kmlem2 8973 axcc2lem 9258 dominf 9267 dcomex 9269 ac4c 9298 ac5 9299 dominfac 9395 pwfseqlem4 9484 grothomex 9651 ramub2 15718 ismred2 16263 utopsnneiplem 22051 dvfsumlem2 23790 plydivlem4 24051 bnj865 30993 bnj1015 31031 frmin 31739 poimirlem13 33422 poimirlem14 33423 poimirlem17 33426 poimirlem20 33429 poimirlem25 33434 poimirlem28 33437 poimirlem31 33440 poimirlem32 33441 voliunnfl 33453 volsupnfl 33454 prdsbnd2 33594 iscringd 33797 monotoddzzfi 37507 monotoddzz 37508 frege104 38261 dvgrat 38511 cvgdvgrat 38512 wessf1ornlem 39371 xrlexaddrp 39568 infleinf 39588 dvnmul 40158 dvnprodlem2 40162 fourierdlem41 40365 fourierdlem48 40371 fourierdlem49 40372 fourierdlem51 40374 fourierdlem71 40394 fourierdlem83 40406 fourierdlem97 40420 etransclem2 40453 etransclem46 40497 isomenndlem 40744 ovnsubaddlem1 40784 hoidmvlelem3 40811 vonicclem2 40898 smflimlem1 40979 smflimlem2 40980 smflimlem3 40981 |
Copyright terms: Public domain | W3C validator |