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 3345 with a disjoint variable condition, which does not require ax-13 2372. (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 2899 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2899 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvralw.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvralw.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvralw.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvralfw 3335 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 Ⅎwnf 1790 ∀wral 3053 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-11 2162 ax-12 2179 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-nf 1791 df-clel 2811 df-nfc 2881 df-ral 3058 |
This theorem is referenced by: cbvralsvw 3368 cbviin 4923 disjxun 5028 ralxpf 5689 eqfnfv2f 6813 ralrnmptw 6870 dff13f 7025 ofrfval2 7445 fmpox 7790 ovmptss 7814 cbvixp 8524 mptelixpg 8545 boxcutc 8551 xpf1o 8729 indexfi 8905 ixpiunwdom 9127 dfac8clem 9532 acni2 9546 ac6c4 9981 iundom2g 10040 uniimadomf 10045 rabssnn0fi 13445 rlim2 14943 ello1mpt 14968 o1compt 15034 fsum00 15246 iserodd 16272 pcmptdvds 16330 catpropd 17083 invfuc 17349 gsummptnn0fz 19225 gsummoncoe1 21079 gsumply1eq 21080 fiuncmp 22155 elptr2 22325 ptcld 22364 ptclsg 22366 ptcnplem 22372 cnmpt11 22414 cnmpt21 22422 ovoliunlem3 24256 ovoliun 24257 ovoliun2 24258 finiunmbl 24296 volfiniun 24299 iunmbl 24305 voliun 24306 mbfeqalem1 24393 mbfsup 24416 mbfinf 24417 mbflim 24420 itg2split 24502 itgeqa 24566 itgfsum 24579 itgabs 24587 itggt0 24596 limciun 24646 dvlipcn 24746 dvfsumlem4 24781 dvfsum2 24786 itgsubst 24801 coeeq2 24991 ulmss 25144 leibpi 25680 rlimcnp 25703 o1cxp 25712 lgamgulmlem6 25771 fsumdvdscom 25922 lgseisenlem2 26112 disjunsn 30507 bnj110 32409 bnj1529 32621 poimirlem23 35423 itgabsnc 35469 itggt0cn 35470 totbndbnd 35570 disjinfi 42269 fmptf 42320 climinff 42694 idlimc 42709 fnlimabslt 42762 limsupref 42768 limsupbnd1f 42769 climbddf 42770 climinf2 42790 limsupubuz 42796 climinfmpt 42798 limsupmnf 42804 limsupre2 42808 limsupmnfuz 42810 limsupre3 42816 limsupre3uz 42819 limsupreuz 42820 climuz 42827 lmbr3 42830 limsupgt 42861 liminfreuz 42886 liminflt 42888 xlimpnfxnegmnf 42897 xlimmnf 42924 xlimpnf 42925 dfxlim2 42931 cncfshift 42957 stoweidlem31 43114 iundjiun 43540 meaiunincf 43563 pimgtmnf2 43790 smfpimcc 43880 smfsup 43886 smfinflem 43889 smfinf 43890 cbvral2 44127 |
Copyright terms: Public domain | W3C validator |