|   | 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.) Avoid ax-10 2140 and ax-11 2156. (Revised by GG, 20-Aug-2023.) | 
| Ref | Expression | 
|---|---|
| vtoclga.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | 
| vtoclga.2 | ⊢ (𝑥 ∈ 𝐵 → 𝜑) | 
| Ref | Expression | 
|---|---|
| vtoclga | ⊢ (𝐴 ∈ 𝐵 → 𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | eleq1 2828 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 2 | vtoclga.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 3 | 1, 2 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) | 
| 4 | vtoclga.2 | . . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
| 5 | 3, 4 | vtoclg 3553 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓)) | 
| 6 | 5 | pm2.43i 52 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1539 ∈ wcel 2107 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 | 
| This theorem is referenced by: vtocl2ga 3577 vtocl3ga 3582 vtoclri 3589 disjxiun 5139 wfis3 6381 opabiota 6990 fvmpt3 7019 fvmptss 7027 fnressn 7177 fressnfv 7179 caovord 7645 caovmo 7671 ordunisuc 7853 tfis3 7880 fpr2a 8328 frrdmcl 8334 wfr2aOLD 8367 onfununi 8382 smogt 8408 tz7.44-1 8447 tz7.44-2 8448 tz7.44-3 8449 nnacl 8650 nnmcl 8651 nnecl 8652 nnacom 8656 nnaass 8661 nndi 8662 nnmass 8663 nnmsucr 8664 nnmcom 8665 nnmordi 8670 ixpfn 8944 findcard 9204 findcard2 9205 marypha1 9475 cantnfle 9712 cantnflem1 9730 cnfcom 9741 frr2 9801 fseqenlem1 10065 nnadju 10239 ackbij1lem8 10267 cardcf 10293 cfsmolem 10311 wunex2 10779 ingru 10856 recrecnq 11008 prlem934 11074 nn1suc 12289 uzind4s2 12952 rpnnen1lem6 13025 cnref1o 13028 xmulasslem 13328 om2uzsuci 13990 expcl2lem 14115 hashpw 14476 seqcoll 14504 climub 15699 climserle 15700 sumrblem 15748 fsumcvg 15749 summolem2a 15752 infcvgaux2i 15895 prodfn0 15931 prodfrec 15932 prodrblem 15966 fprodcvg 15967 prodmolem2a 15971 divalglem8 16438 bezoutlem1 16577 alginv 16613 algcvg 16614 algcvga 16617 algfx 16618 prmind2 16723 prmpwdvds 16943 cnextfvval 24074 xrsxmet 24832 xrhmeo 24978 cmetcaulem 25323 bcth3 25366 itg2addlem 25794 taylfval 26401 sinord 26577 logexprlim 27270 lgsdir2lem4 27373 noseqind 28299 hlim2 31212 elnlfn 31948 lnconi 32053 chirredlem3 32412 chirredlem4 32413 cnre2csqlem 33910 eulerpartlemsf 34362 eulerpartlemn 34384 bnj1321 35042 bnj1418 35055 subfacp1lem1 35185 nn0prpwlem 36324 findreccl 36455 weiunlem2 36465 mptsnunlem 37340 rdgeqoa 37372 domalom 37406 poimirlem22 37650 poimirlem26 37654 mblfinlem3 37667 mblfinlem4 37668 ismblfin 37669 ftc1anclem3 37703 ftc1anclem8 37708 sdclem2 37750 iscringd 38006 renegclALT 38965 zindbi 42963 fmuldfeq 45603 sumnnodd 45650 iblspltprt 45993 stoweidlem2 46022 stoweidlem17 46037 stoweidlem21 46041 stoweidlem43 46063 stoweidlem51 46071 wallispi 46090 upwordisword 46901 | 
| Copyright terms: Public domain | W3C validator |