![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclbg | Structured version Visualization version Unicode version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
vtoclbg.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtoclbg.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtoclbg.3 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
vtoclbg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtoclbg.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | vtoclbg.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bibi12d 328 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | vtoclbg.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | vtoclg 3093 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-12 1950 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-v 3033 |
This theorem is referenced by: alexeqg 3156 pm13.183 3167 sbc8g 3263 sbc2or 3264 sbcco 3278 sbc5 3280 sbcie2g 3289 eqsbc3 3295 sbcng 3296 sbcimg 3297 sbcan 3298 sbcor 3299 sbcbig 3300 sbcal 3305 sbcex2 3306 sbcel1v 3314 sbcreu 3332 csbiebg 3372 sbcel12 3776 sbceqg 3777 elpwg 3950 snssg 4096 preq12bg 4146 elintg 4234 elintrabg 4239 sbcbr123 4447 opelresg 5118 inisegn0 5206 funfvima3 6160 elixpsn 7579 ixpsnf1o 7580 domeng 7601 1sdom 7793 rankcf 9220 pt1hmeo 20898 eldm3 30473 br1steqg 30487 br2ndeqg 30488 elima4 30492 brsset 30727 brbigcup 30736 elfix2 30742 elfunsg 30754 elsingles 30756 funpartlem 30780 ellines 30990 elhf2g 31014 cover2g 32105 sbcrexgOLD 35699 sbcangOLD 36960 sbcorgOLD 36961 sbcalgOLD 36973 sbcexgOLD 36974 sbcel12gOLD 36975 sbcel1gvOLD 37318 |
Copyright terms: Public domain | W3C validator |