![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvral | Structured version Visualization version GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 31-Jul-2003.) |
Ref | Expression |
---|---|
cbvral.1 | ⊢ Ⅎ𝑦𝜑 |
cbvral.2 | ⊢ Ⅎ𝑥𝜓 |
cbvral.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvral | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2902 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2902 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvral.1 | . 2 ⊢ Ⅎ𝑦𝜑 | |
4 | cbvral.2 | . 2 ⊢ Ⅎ𝑥𝜓 | |
5 | cbvral.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvralf 3304 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 Ⅎwnf 1857 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clel 2756 df-nfc 2891 df-ral 3055 |
This theorem is referenced by: cbvralv 3310 cbvralsv 3321 cbviin 4710 disjxun 4802 ralxpf 5424 eqfnfv2f 6479 ralrnmpt 6532 dff13f 6677 ofrfval2 7081 fmpt2x 7405 ovmptss 7427 cbvixp 8093 mptelixpg 8113 boxcutc 8119 xpf1o 8289 indexfi 8441 ixpiunwdom 8663 dfac8clem 9065 acni2 9079 ac6num 9513 ac6c4 9515 iundom2g 9574 uniimadomf 9579 rabssnn0fi 12999 rlim2 14446 ello1mpt 14471 o1compt 14537 fsum00 14749 iserodd 15762 pcmptdvds 15820 catpropd 16590 invfuc 16855 gsummptnn0fz 18602 gsummoncoe1 19896 gsumply1eq 19897 fiuncmp 21429 elptr2 21599 ptcld 21638 ptclsg 21640 ptcnplem 21646 cnmpt11 21688 cnmpt21 21696 ovoliunlem3 23492 ovoliun 23493 ovoliun2 23494 finiunmbl 23532 volfiniun 23535 iunmbl 23541 voliun 23542 mbfeqalem 23628 mbfsup 23650 mbfinf 23651 mbflim 23654 itg2split 23735 itgeqa 23799 itgfsum 23812 itgabs 23820 itggt0 23827 limciun 23877 dvlipcn 23976 dvfsumlem4 24011 dvfsum2 24016 itgsubst 24031 coeeq2 24217 ulmss 24370 leibpi 24889 rlimcnp 24912 o1cxp 24921 lgamgulmlem6 24980 fsumdvdscom 25131 lgseisenlem2 25321 disjunsn 29735 bnj110 31256 bnj1529 31466 poimirlem23 33763 itgabsnc 33810 itggt0cn 33813 totbndbnd 33919 disjinfi 39897 fmptf 39965 climinff 40364 idlimc 40379 fnlimabslt 40432 limsupref 40438 limsupbnd1f 40439 climbddf 40440 climinf2 40460 limsupubuz 40466 climinfmpt 40468 limsupmnf 40474 limsupre2 40478 limsupmnfuz 40480 limsupre3 40486 limsupre3uz 40489 limsupreuz 40490 climuz 40497 lmbr3 40500 liminflelimsup 40529 limsupgt 40531 liminfreuz 40556 liminflt 40558 xlimmnf 40588 xlimpnf 40589 dfxlim2 40595 cncfshift 40608 stoweidlem31 40769 iundjiun 41198 meaiunincf 41221 pimgtmnf2 41448 smfpimcc 41538 smfsup 41544 smfinflem 41547 smfinf 41548 cbvral2 41696 |
Copyright terms: Public domain | W3C validator |