| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvralw | Structured version Visualization version GIF version | ||
| Description: Rule used to change bound variables, using implicit substitution. Version of cbvralfw 3304 with more disjoint variable conditions. (Contributed by NM, 31-Jul-2003.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.) |
| Ref | Expression |
|---|---|
| cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
| cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
| cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvralw | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfcv 2905 | . 2 ⊢ Ⅎ𝑥𝐴 | |
| 2 | nfcv 2905 | . 2 ⊢ Ⅎ𝑦𝐴 | |
| 3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
| 4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
| 5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 6 | 1, 2, 3, 4, 5 | cbvralfw 3304 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 Ⅎwnf 1783 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-11 2157 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-nf 1784 df-clel 2816 df-nfc 2892 df-ral 3062 |
| This theorem is referenced by: cbvralsvwOLD 3319 cbvralsvwOLDOLD 3320 cbviin 5037 disjxun 5141 ralxpf 5857 eqfnfv2f 7055 ralrnmptw 7114 dff13f 7276 ofrfval2 7718 fmpox 8092 ovmptss 8118 cbvixp 8954 mptelixpg 8975 boxcutc 8981 xpf1o 9179 indexfi 9400 ixpiunwdom 9630 dfac8clem 10072 acni2 10086 ac6c4 10521 iundom2g 10580 uniimadomf 10585 rabssnn0fi 14027 rlim2 15532 ello1mpt 15557 o1compt 15623 fsum00 15834 iserodd 16873 pcmptdvds 16932 catpropd 17752 invfuc 18022 gsummptnn0fz 20004 gsummoncoe1 22312 gsumply1eq 22313 fiuncmp 23412 elptr2 23582 ptcld 23621 ptclsg 23623 ptcnplem 23629 cnmpt11 23671 cnmpt21 23679 ovoliunlem3 25539 ovoliun 25540 ovoliun2 25541 finiunmbl 25579 volfiniun 25582 iunmbl 25588 voliun 25589 mbfeqalem1 25676 mbfsup 25699 mbfinf 25700 mbflim 25703 itg2split 25784 itgeqa 25849 itgfsum 25862 itgabs 25870 itggt0 25879 limciun 25929 dvlipcn 26033 dvfsumlem4 26070 dvfsum2 26075 itgsubst 26090 coeeq2 26281 ulmss 26440 leibpi 26985 rlimcnp 27008 o1cxp 27018 lgamgulmlem6 27077 fsumdvdscom 27228 lgseisenlem2 27420 disjunsn 32607 bnj110 34872 bnj1529 35084 weiunpo 36466 weiunso 36467 weiunfr 36468 weiunse 36469 poimirlem23 37650 itgabsnc 37696 itggt0cn 37697 totbndbnd 37796 aks6d1c1p5 42113 aks6d1c1rh 42126 aks6d1c7 42185 unitscyglem3 42198 disjinfi 45197 fmptf 45245 caucvgbf 45500 climinff 45626 idlimc 45641 fnlimabslt 45694 limsupref 45700 limsupbnd1f 45701 climbddf 45702 climinf2 45722 limsupubuz 45728 climinfmpt 45730 limsupmnf 45736 limsupre2 45740 limsupmnfuz 45742 limsupre3 45748 limsupre3uz 45751 limsupreuz 45752 climuz 45759 lmbr3 45762 limsupgt 45793 liminfreuz 45818 liminflt 45820 xlimpnfxnegmnf 45829 xlimmnf 45856 xlimpnf 45857 dfxlim2 45863 cncfshift 45889 stoweidlem31 46046 iundjiun 46475 meaiunincf 46498 pimgtmnf2 46729 smfpimcc 46823 smfsup 46829 smfinflem 46832 smfinf 46833 cbvral2 47115 |
| Copyright terms: Public domain | W3C validator |