Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iuneq1 | Structured version Visualization version GIF version |
Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
iuneq1 | ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iunss1 4933 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶) | |
2 | iunss1 4933 | . . 3 ⊢ (𝐵 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶) | |
3 | 1, 2 | anim12i 614 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)) |
4 | eqss 3982 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
5 | eqss 3982 | . 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)) | |
6 | 3, 4, 5 | 3imtr4i 294 | 1 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1537 ⊆ wss 3936 ∪ ciun 4919 |
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-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rex 3144 df-v 3496 df-in 3943 df-ss 3952 df-iun 4921 |
This theorem is referenced by: iuneq1d 4946 iinvdif 5002 iunxprg 5018 iununi 5021 iunsuc 6273 funopsn 6910 funiunfv 7007 onfununi 7978 iunfi 8812 rankuni2b 9282 pwsdompw 9626 ackbij1lem7 9648 r1om 9666 fictb 9667 cfsmolem 9692 ituniiun 9844 domtriomlem 9864 domtriom 9865 inar1 10197 fsum2d 15126 fsumiun 15176 ackbijnn 15183 fprod2d 15335 prmreclem5 16256 lpival 20018 fiuncmp 22012 ovolfiniun 24102 ovoliunnul 24108 finiunmbl 24145 volfiniun 24148 voliunlem1 24151 iuninc 30312 ofpreima2 30411 esum2dlem 31351 sigaclfu2 31380 sigapildsyslem 31420 fiunelros 31433 bnj548 32169 bnj554 32171 bnj594 32184 trpredlem1 33066 trpredtr 33069 trpredmintr 33070 trpredrec 33077 neibastop2lem 33708 istotbnd3 35064 0totbnd 35066 sstotbnd2 35067 sstotbnd 35068 sstotbnd3 35069 totbndbnd 35082 prdstotbnd 35087 cntotbnd 35089 heibor 35114 dfrcl4 40041 iunrelexp0 40067 comptiunov2i 40071 corclrcl 40072 cotrcltrcl 40090 trclfvdecomr 40093 dfrtrcl4 40103 corcltrcl 40104 cotrclrcl 40107 fiiuncl 41347 iuneq1i 41370 sge0iunmptlemfi 42715 caragenfiiuncl 42817 carageniuncllem1 42823 ovnsubadd2lem 42947 |
Copyright terms: Public domain | W3C validator |