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 2141 and ax-11 2158. (Revised by Gino Giotto, 20-Aug-2023.) |
Ref | Expression |
---|---|
vtoclga.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
vtoclga.2 | ⊢ (𝑥 ∈ 𝐵 → 𝜑) |
Ref | Expression |
---|---|
vtoclga | ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2825 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
2 | vtoclga.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
3 | 1, 2 | imbi12d 348 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓))) |
4 | vtoclga.2 | . . 3 ⊢ (𝑥 ∈ 𝐵 → 𝜑) | |
5 | 3, 4 | vtoclg 3481 | . 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 → 𝜓)) |
6 | 5 | pm2.43i 52 | 1 ⊢ (𝐴 ∈ 𝐵 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1543 ∈ wcel 2110 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 |
This theorem is referenced by: vtocl2ga 3490 vtoclri 3501 disjxiun 5050 wfis3 6211 opabiota 6794 fvmpt3 6822 fvmptss 6830 fnressn 6973 fressnfv 6975 caovord 7419 caovmo 7445 ordunisuc 7611 tfis3 7636 fpr2 8044 wfr2a 8072 onfununi 8078 smogt 8104 tz7.44-1 8142 tz7.44-2 8143 tz7.44-3 8144 nnacl 8339 nnmcl 8340 nnecl 8341 nnacom 8345 nnaass 8350 nndi 8351 nnmass 8352 nnmsucr 8353 nnmcom 8354 nnmordi 8359 ixpfn 8584 findcard 8841 findcard2 8842 findcard2OLD 8913 marypha1 9050 cantnfle 9286 cantnflem1 9304 cnfcom 9315 frr2 9376 fseqenlem1 9638 nnadju 9811 ackbij1lem8 9841 cardcf 9866 cfsmolem 9884 wunex2 10352 ingru 10429 recrecnq 10581 prlem934 10647 nn1suc 11852 uzind4s2 12505 rpnnen1lem6 12578 cnref1o 12581 xmulasslem 12875 om2uzsuci 13521 expcl2lem 13647 hashpw 14003 seqcoll 14030 climub 15225 climserle 15226 sumrblem 15275 fsumcvg 15276 summolem2a 15279 infcvgaux2i 15422 prodfn0 15458 prodfrec 15459 prodrblem 15491 fprodcvg 15492 prodmolem2a 15496 divalglem8 15961 bezoutlem1 16099 alginv 16132 algcvg 16133 algcvga 16136 algfx 16137 prmind2 16242 prmpwdvds 16457 cnextfvval 22962 xrsxmet 23706 xrhmeo 23843 cmetcaulem 24185 bcth3 24228 itg2addlem 24656 taylfval 25251 sinord 25423 logexprlim 26106 lgsdir2lem4 26209 hlim2 29273 elnlfn 30009 lnconi 30114 chirredlem3 30473 chirredlem4 30474 cnre2csqlem 31574 eulerpartlemsf 32038 eulerpartlemn 32060 bnj1321 32720 bnj1418 32733 subfacp1lem1 32854 nn0prpwlem 34248 findreccl 34379 mptsnunlem 35246 rdgeqoa 35278 domalom 35312 poimirlem22 35536 poimirlem26 35540 mblfinlem3 35553 mblfinlem4 35554 ismblfin 35555 ftc1anclem3 35589 ftc1anclem8 35594 sdclem2 35637 iscringd 35893 renegclALT 36714 zindbi 40471 fmuldfeq 42799 sumnnodd 42846 iblspltprt 43189 stoweidlem2 43218 stoweidlem17 43233 stoweidlem21 43237 stoweidlem43 43259 stoweidlem51 43267 wallispi 43286 |
Copyright terms: Public domain | W3C validator |