Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvixpv | Structured version Visualization version GIF version |
Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Ref | Expression |
---|---|
cbvixpv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvixpv | ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2907 | . 2 ⊢ Ⅎ𝑦𝐵 | |
2 | nfcv 2907 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | cbvixpv.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
4 | 1, 2, 3 | cbvixp 8619 | 1 ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 Xcixp 8602 |
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 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ral 3069 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4255 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-iota 6359 df-fn 6404 df-fv 6409 df-ixp 8603 |
This theorem is referenced by: funcpropd 17440 invfuc 17516 natpropd 17518 dprdw 19430 dprdwd 19431 ptuni2 22505 ptbasin 22506 ptbasfi 22510 ptpjopn 22541 ptclsg 22544 dfac14 22547 ptcnp 22551 ptcmplem2 22982 ptcmpg 22986 prdsxmslem2 23459 upixp 35661 rrxsnicc 43562 ioorrnopn 43567 ioorrnopnxr 43569 ovnsubadd 43831 hoidmvlelem4 43857 hoidmvle 43859 hspdifhsp 43875 hoiqssbllem2 43882 hspmbl 43888 hoimbl 43890 opnvonmbl 43893 ovnovollem3 43917 |
Copyright terms: Public domain | W3C validator |