![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iuneq2d | Structured version Visualization version GIF version |
Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.) |
Ref | Expression |
---|---|
iuneq2d.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
iuneq2d | ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq2d.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
2 | 1 | adantr 466 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | iuneq2dv 4677 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 ∈ wcel 2145 ∪ ciun 4655 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-v 3353 df-in 3730 df-ss 3737 df-iun 4657 |
This theorem is referenced by: iununi 4745 oelim2 7833 ituniiun 9450 dfrtrclrec2 14005 rtrclreclem1 14006 rtrclreclem2 14007 rtrclreclem4 14009 imasval 16379 mreacs 16526 cnextval 22085 taylfval 24333 iunpreima 29721 reprdifc 31045 msubvrs 31795 trpredeq1 32056 trpredeq2 32057 neibastop2 32693 voliunnfl 33786 sstotbnd2 33905 equivtotbnd 33909 totbndbnd 33920 heiborlem3 33944 eliunov2 38497 fvmptiunrelexplb0d 38502 fvmptiunrelexplb1d 38504 comptiunov2i 38524 trclrelexplem 38529 dftrcl3 38538 trclfvcom 38541 cnvtrclfv 38542 cotrcltrcl 38543 trclimalb2 38544 trclfvdecomr 38546 dfrtrcl3 38551 dfrtrcl4 38556 isomenndlem 41261 ovnval 41272 hoicvr 41279 hoicvrrex 41287 ovnlecvr 41289 ovncvrrp 41295 ovnsubaddlem1 41301 hoidmvlelem3 41328 hoidmvle 41331 ovnhoilem1 41332 ovnovollem1 41387 smflimlem3 41498 otiunsndisjX 41818 |
Copyright terms: Public domain | W3C validator |