![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclga | Structured version Visualization version GIF version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
vtoclga.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclga.2 | ⊢ (𝑥 ∈ 𝐵 → 𝜑) |
Ref | Expression |
---|---|
vtoclga | ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2903 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1993 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclga.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclga.2 | . 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 1, 2, 3, 4 | vtoclgaf 3412 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1632 ∈ wcel 2140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1989 ax-6 2055 ax-7 2091 ax-9 2149 ax-10 2169 ax-11 2184 ax-12 2197 ax-13 2392 ax-ext 2741 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2048 df-clab 2748 df-cleq 2754 df-clel 2757 df-nfc 2892 df-v 3343 |
This theorem is referenced by: vtoclri 3424 ssuniOLD 4613 disjxiun 4802 wfis3 5883 opabiota 6425 fvmpt3 6450 fvmptss 6456 fnressn 6590 fressnfv 6592 caovord 7012 caovmo 7038 ordunisuc 7199 tfis3 7224 wfr2a 7603 onfununi 7609 smogt 7635 tz7.44-1 7673 tz7.44-2 7674 tz7.44-3 7675 nnacl 7863 nnmcl 7864 nnecl 7865 nnacom 7869 nnaass 7874 nndi 7875 nnmass 7876 nnmsucr 7877 nnmcom 7878 nnmordi 7883 ixpfn 8083 findcard 8367 findcard2 8368 marypha1 8508 cantnfle 8744 cantnflem1 8762 cnfcom 8773 fseqenlem1 9058 ackbij1lem5 9259 ackbij1lem8 9262 cardcf 9287 cfsmolem 9305 wunex2 9773 ingru 9850 recrecnq 10002 prlem934 10068 nn1suc 11254 uzind4s2 11963 rpnnen1lem6 12033 rpnnen1OLD 12039 cnref1o 12041 xmulasslem 12329 om2uzsuci 12962 expcl2lem 13087 hashmap 13435 hashpw 13436 seqcoll 13461 climub 14612 climserle 14613 sumrblem 14662 fsumcvg 14663 summolem2a 14666 infcvgaux2i 14810 prodfn0 14846 prodfrec 14847 prodrblem 14879 fprodcvg 14880 prodmolem2a 14884 divalglem8 15346 bezoutlem1 15479 alginv 15511 algcvg 15512 algcvga 15515 algfx 15516 prmind2 15621 prmpwdvds 15831 cnextfvval 22091 xrsxmet 22834 xrhmeo 22967 cmetcaulem 23307 bcth3 23349 itg2addlem 23745 taylfval 24333 sinord 24501 logexprlim 25171 lgsdir2lem4 25274 hlim2 28380 elnlfn 29118 lnconi 29223 chirredlem3 29582 chirredlem4 29583 cnre2csqlem 30287 eulerpartlemsf 30752 eulerpartlemn 30774 bnj1321 31424 bnj1418 31437 subfacp1lem1 31490 frins3 32079 nn0prpwlem 32645 findreccl 32780 mptsnunlem 33515 rdgeqoa 33548 poimirlem22 33763 poimirlem26 33767 mblfinlem3 33780 mblfinlem4 33781 ismblfin 33782 ftc1anclem3 33819 ftc1anclem8 33824 sdclem2 33870 iscringd 34129 renegclALT 34771 zindbi 38032 fmuldfeq 40337 sumnnodd 40384 iblspltprt 40711 stoweidlem2 40741 stoweidlem17 40756 stoweidlem21 40760 stoweidlem43 40782 stoweidlem51 40790 wallispi 40809 |
Copyright terms: Public domain | W3C validator |