![]() |
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 2900 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfv 1990 | . 2 ⊢ Ⅎ𝑥𝜓 | |
3 | vtoclga.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | vtoclga.2 | . 2 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 1, 2, 3, 4 | vtoclgaf 3409 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1630 ∈ wcel 2137 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-v 3340 |
This theorem is referenced by: vtoclri 3421 ssuniOLD 4610 disjxiun 4799 wfis3 5880 opabiota 6421 fvmpt3 6446 fvmptss 6452 fnressn 6586 fressnfv 6588 caovord 7008 caovmo 7034 ordunisuc 7195 tfis3 7220 wfr2a 7599 onfununi 7605 smogt 7631 tz7.44-1 7669 tz7.44-2 7670 tz7.44-3 7671 nnacl 7858 nnmcl 7859 nnecl 7860 nnacom 7864 nnaass 7869 nndi 7870 nnmass 7871 nnmsucr 7872 nnmcom 7873 nnmordi 7878 ixpfn 8078 findcard 8362 findcard2 8363 marypha1 8503 cantnfle 8739 cantnflem1 8757 cnfcom 8768 fseqenlem1 9035 ackbij1lem5 9236 ackbij1lem8 9239 cardcf 9264 cfsmolem 9282 wunex2 9750 ingru 9827 recrecnq 9979 prlem934 10045 nn1suc 11231 uzind4s2 11940 rpnnen1lem6 12010 rpnnen1OLD 12016 cnref1o 12018 xmulasslem 12306 om2uzsuci 12939 expcl2lem 13064 hashmap 13412 hashpw 13413 seqcoll 13438 climub 14589 climserle 14590 sumrblem 14639 fsumcvg 14640 summolem2a 14643 infcvgaux2i 14787 prodfn0 14823 prodfrec 14824 prodrblem 14856 fprodcvg 14857 prodmolem2a 14861 divalglem8 15323 bezoutlem1 15456 alginv 15488 algcvg 15489 algcvga 15492 algfx 15493 prmind2 15598 prmpwdvds 15808 cnextfvval 22068 xrsxmet 22811 xrhmeo 22944 cmetcaulem 23284 bcth3 23326 itg2addlem 23722 taylfval 24310 sinord 24477 logexprlim 25147 lgsdir2lem4 25250 hlim2 28356 elnlfn 29094 lnconi 29199 chirredlem3 29558 chirredlem4 29559 cnre2csqlem 30263 eulerpartlemsf 30728 eulerpartlemn 30750 bnj1321 31400 bnj1418 31413 subfacp1lem1 31466 frins3 32055 nn0prpwlem 32621 findreccl 32756 mptsnunlem 33494 rdgeqoa 33527 poimirlem22 33742 poimirlem26 33746 mblfinlem3 33759 mblfinlem4 33760 ismblfin 33761 ftc1anclem3 33798 ftc1anclem8 33803 sdclem2 33849 iscringd 34108 renegclALT 34750 zindbi 38011 fmuldfeq 40316 sumnnodd 40363 iblspltprt 40690 stoweidlem2 40720 stoweidlem17 40735 stoweidlem21 40739 stoweidlem43 40761 stoweidlem51 40769 wallispi 40788 |
Copyright terms: Public domain | W3C validator |