![]() |
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 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | iuneq2dv 5015 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 ∪ ciun 4991 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 df-rex 3066 df-v 3471 df-in 3951 df-ss 3961 df-iun 4993 |
This theorem is referenced by: iununi 5096 oelim2 8609 ituniiun 10439 rtrclreclem1 15030 dfrtrclrec2 15031 rtrclreclem2 15032 rtrclreclem4 15034 imasval 17486 mreacs 17631 pzriprnglem10 21409 cnextval 23958 taylfval 26286 iunpreima 32348 reprdifc 34249 msubvrs 35160 neibastop2 35835 voliunnfl 37126 sstotbnd2 37236 equivtotbnd 37240 totbndbnd 37251 heiborlem3 37275 eliunov2 43081 fvmptiunrelexplb0d 43086 fvmptiunrelexplb1d 43088 comptiunov2i 43108 trclrelexplem 43113 dftrcl3 43122 trclfvcom 43125 cnvtrclfv 43126 cotrcltrcl 43127 trclimalb2 43128 trclfvdecomr 43130 dfrtrcl3 43135 dfrtrcl4 43140 isomenndlem 45890 ovnval 45901 hoicvr 45908 hoicvrrex 45916 ovnlecvr 45918 ovncvrrp 45924 ovnsubaddlem1 45930 hoidmvlelem3 45957 hoidmvle 45960 ovnhoilem1 45961 ovnovollem1 46016 smflimlem3 46133 otiunsndisjX 46631 |
Copyright terms: Public domain | W3C validator |