Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > vtocl2g | Structured version Visualization version Unicode version |
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.) |
Ref | Expression |
---|---|
vtocl2g.1 | |
vtocl2g.2 | |
vtocl2g.3 |
Ref | Expression |
---|---|
vtocl2g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2764 | . 2 | |
2 | nfcv 2764 | . 2 | |
3 | nfcv 2764 | . 2 | |
4 | nfv 1843 | . 2 | |
5 | nfv 1843 | . 2 | |
6 | vtocl2g.1 | . 2 | |
7 | vtocl2g.2 | . 2 | |
8 | vtocl2g.3 | . 2 | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | vtocl2gf 3268 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wcel 1990 |
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-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 |
This theorem is referenced by: vtocl4g 3277 ifexg 4157 uniprg 4450 intprg 4511 opthg 4946 opelopabsb 4985 vtoclr 5164 elimasng 5491 cnvsng 5621 funopg 5922 f1osng 6177 fsng 6404 fvsng 6447 fnpr2g 6474 unexb 6958 op1stg 7180 op2ndg 7181 xpsneng 8045 xpcomeng 8052 sbth 8080 unxpdom 8167 fpwwe2lem5 9456 prcdnq 9815 mhmlem 17535 carsgmon 30376 br1steqgOLD 31674 br2ndeqgOLD 31675 brimageg 32034 brdomaing 32042 brrangeg 32043 rankung 32273 mbfresfi 33456 zindbi 37511 2sbc6g 38616 2sbc5g 38617 fmulcl 39813 |
Copyright terms: Public domain | W3C validator |