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 cbvral 3445 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvralw.1 | ⊢ Ⅎ𝑦𝜑 |
cbvralw.2 | ⊢ Ⅎ𝑥𝜓 |
cbvralw.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvralw | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2977 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2977 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvralfw 3437 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 Ⅎwnf 1784 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-10 2145 ax-11 2161 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 df-sb 2070 df-clel 2893 df-nfc 2963 df-ral 3143 |
This theorem is referenced by: cbvralsvw 3467 cbviin 4962 disjxun 5064 ralxpf 5717 eqfnfv2f 6806 ralrnmptw 6860 dff13f 7014 ofrfval2 7427 fmpox 7765 ovmptss 7788 cbvixp 8478 mptelixpg 8499 boxcutc 8505 xpf1o 8679 indexfi 8832 ixpiunwdom 9055 dfac8clem 9458 acni2 9472 ac6c4 9903 iundom2g 9962 uniimadomf 9967 rabssnn0fi 13355 rlim2 14853 ello1mpt 14878 o1compt 14944 fsum00 15153 iserodd 16172 pcmptdvds 16230 catpropd 16979 invfuc 17244 gsummptnn0fz 19106 gsummoncoe1 20472 gsumply1eq 20473 fiuncmp 22012 elptr2 22182 ptcld 22221 ptclsg 22223 ptcnplem 22229 cnmpt11 22271 cnmpt21 22279 ovoliunlem3 24105 ovoliun 24106 ovoliun2 24107 finiunmbl 24145 volfiniun 24148 iunmbl 24154 voliun 24155 mbfeqalem1 24242 mbfsup 24265 mbfinf 24266 mbflim 24269 itg2split 24350 itgeqa 24414 itgfsum 24427 itgabs 24435 itggt0 24442 limciun 24492 dvlipcn 24591 dvfsumlem4 24626 dvfsum2 24631 itgsubst 24646 coeeq2 24832 ulmss 24985 leibpi 25520 rlimcnp 25543 o1cxp 25552 lgamgulmlem6 25611 fsumdvdscom 25762 lgseisenlem2 25952 disjunsn 30344 bnj110 32130 bnj1529 32342 poimirlem23 34930 itgabsnc 34976 itggt0cn 34979 totbndbnd 35082 disjinfi 41503 fmptf 41558 climinff 41941 idlimc 41956 fnlimabslt 42009 limsupref 42015 limsupbnd1f 42016 climbddf 42017 climinf2 42037 limsupubuz 42043 climinfmpt 42045 limsupmnf 42051 limsupre2 42055 limsupmnfuz 42057 limsupre3 42063 limsupre3uz 42066 limsupreuz 42067 climuz 42074 lmbr3 42077 limsupgt 42108 liminfreuz 42133 liminflt 42135 xlimpnfxnegmnf 42144 xlimmnf 42171 xlimpnf 42172 dfxlim2 42178 cncfshift 42206 stoweidlem31 42365 iundjiun 42791 meaiunincf 42814 pimgtmnf2 43041 smfpimcc 43131 smfsup 43137 smfinflem 43140 smfinf 43141 |
Copyright terms: Public domain | W3C validator |