![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > vtocl2g | Unicode version |
Description: Implicit substitution of 2 classes for 2 set variables. (Contributed by NM, 25-Apr-1995.) |
Ref | Expression |
---|---|
vtocl2g.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtocl2g.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtocl2g.3 |
![]() ![]() |
Ref | Expression |
---|---|
vtocl2g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2548 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2548 |
. 2
![]() ![]() ![]() ![]() | |
3 | nfcv 2548 |
. 2
![]() ![]() ![]() ![]() | |
4 | nfv 1626 |
. 2
![]() ![]() ![]() ![]() | |
5 | nfv 1626 |
. 2
![]() ![]() ![]() ![]() | |
6 | vtocl2g.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | vtocl2g.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | vtocl2g.3 |
. 2
![]() ![]() | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | vtocl2gf 2981 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: ifexg 3766 uniprg 3998 intprg 4052 opthg 4404 opelopabsb 4433 unexb 4676 vtoclr 4889 elimasng 5197 cnvsng 5322 funopg 5452 f1osng 5683 fsng 5874 fvsng 5894 op1stg 6326 op2ndg 6327 xpsneng 7160 xpcomeng 7167 sbth 7194 unxpdom 7283 fpwwe2lem5 8473 prcdnq 8834 2pthoncl 21564 brimageg 25688 brdomaing 25696 brrangeg 25697 rankung 26019 mbfresfi 26160 zindbi 26907 2sbc6g 27491 2sbc5g 27492 fmulcl 27586 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-v 2926 |
Copyright terms: Public domain | W3C validator |