Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iuneq1d | Structured version Visualization version GIF version |
Description: Equality theorem for indexed union, deduction version. (Contributed by Drahflow, 22-Oct-2015.) |
Ref | Expression |
---|---|
iuneq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
iuneq1d | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | iuneq1 4927 | . 2 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∪ ciun 4911 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-v 3496 df-in 3942 df-ss 3951 df-iun 4913 |
This theorem is referenced by: iuneq12d 4939 disjxiun 5055 kmlem11 9580 prmreclem4 16249 imasval 16778 iundisj 24143 iundisj2 24144 voliunlem1 24145 iunmbl 24148 volsup 24151 uniioombllem4 24181 iuninc 30306 iundisjf 30333 iundisj2f 30334 suppovss 30420 iundisjfi 30513 iundisj2fi 30514 iundisjcnt 30515 indval2 31268 sigaclcu3 31376 fiunelros 31428 meascnbl 31473 bnj1113 32052 bnj155 32146 bnj570 32172 bnj893 32195 cvmliftlem10 32536 mrsubvrs 32764 msubvrs 32802 voliunnfl 34930 volsupnfl 34931 heiborlem3 35085 heibor 35093 iunrelexp0 40040 iunp1 41321 iundjiunlem 42735 iundjiun 42736 meaiuninclem 42756 meaiuninc 42757 carageniuncllem1 42797 carageniuncllem2 42798 carageniuncl 42799 caratheodorylem1 42802 caratheodorylem2 42803 |
Copyright terms: Public domain | W3C validator |