Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rspc2v | Structured version Visualization version Unicode version |
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
rspc2v.1 | |
rspc2v.2 |
Ref | Expression |
---|---|
rspc2v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1843 | . 2 | |
2 | nfv 1843 | . 2 | |
3 | rspc2v.1 | . 2 | |
4 | rspc2v.2 | . 2 | |
5 | 1, 2, 3, 4 | rspc2 3320 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wcel 1990 wral 2912 |
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-ral 2917 df-v 3202 |
This theorem is referenced by: rspc2va 3323 rspc3v 3325 disji2 4636 f1veqaeq 6514 isorel 6576 isosolem 6597 oveqrspc2v 6673 fovcl 6765 caovclg 6826 caovcomg 6829 smoel 7457 fiint 8237 dffi3 8337 ltordlem 10553 seqhomo 12848 cshf1 13556 climcn2 14323 drsdir 16935 tsrlin 17219 dirge 17237 mhmlin 17342 issubg2 17609 nsgbi 17625 ghmlin 17665 efgi 18132 efgred 18161 irredmul 18709 issubrg2 18800 abvmul 18829 abvtri 18830 lmodlema 18868 islmodd 18869 rmodislmodlem 18930 rmodislmod 18931 lmhmlin 19035 lbsind 19080 mplcoe5lem 19467 ipcj 19979 obsip 20065 matecl 20231 dmatelnd 20302 scmateALT 20318 mdetdiaglem 20404 mdetdiagid 20406 pmatcoe1fsupp 20506 m2cpminvid2lem 20559 inopn 20704 basis1 20754 basis2 20755 iscldtop 20899 hausnei 21132 t1sep2 21173 nconnsubb 21226 r0sep 21551 fbasssin 21640 fcfneii 21841 ustssel 22009 xmeteq0 22143 tngngp3 22460 nmvs 22480 cncfi 22697 c1lip1 23760 aalioulem3 24089 logltb 24346 cvxcl 24711 2sqlem8 25151 axtgcgrrflx 25361 axtgsegcon 25363 axtg5seg 25364 axtgbtwnid 25365 axtgpasch 25366 axtgcont1 25367 axtgupdim2 25370 axtgeucl 25371 iscgrglt 25409 isperp2d 25611 f1otrgds 25749 brbtwn2 25785 axcontlem3 25846 axcontlem9 25852 axcontlem10 25853 upgrwlkdvdelem 26632 conngrv2edg 27055 frgrwopreglem5ALT 27186 ablocom 27402 nvs 27518 nvtri 27525 phpar2 27678 phpar 27679 shaddcl 28074 shmulcl 28075 cnopc 28772 unop 28774 hmop 28781 cnfnc 28789 adj1 28792 hstel2 29078 stj 29094 stcltr1i 29133 mddmdin0i 29290 cdj3lem1 29293 cdj3lem2b 29296 disji2f 29390 disjif2 29394 disjxpin 29401 fovcld 29440 isoun 29479 archirng 29742 archiexdiv 29744 slmdlema 29756 inelcarsg 30373 sibfof 30402 breprexplema 30708 axtgupdim2OLD 30746 pconncn 31206 nocvxminlem 31893 ivthALT 32330 poimirlem32 33441 ismtycnv 33601 ismtyima 33602 ismtyres 33607 bfplem1 33621 bfplem2 33622 ghomlinOLD 33687 rngohomadd 33768 rngohommul 33769 crngocom 33800 idladdcl 33818 idllmulcl 33819 idlrmulcl 33820 pridl 33836 ispridlc 33869 pridlc 33870 dmnnzd 33874 oposlem 34469 omllaw 34530 hlsuprexch 34667 lautle 35370 ltrnu 35407 tendovalco 36053 ntrkbimka 38336 mullimc 39848 mullimcf 39855 lptre2pt 39872 fourierdlem54 40377 faovcl 41280 icceuelpartlem 41371 iccpartnel 41374 fargshiftf1 41377 sprsymrelfolem2 41743 mgmhmlin 41786 issubmgm2 41790 |
Copyright terms: Public domain | W3C validator |