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 481 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
3 | 2 | iuneq2dv 4934 | 1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∪ ciun 4910 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-v 3494 df-in 3940 df-ss 3949 df-iun 4912 |
This theorem is referenced by: iununi 5012 oelim2 8210 ituniiun 9832 dfrtrclrec2 14404 rtrclreclem1 14405 rtrclreclem2 14406 rtrclreclem4 14408 imasval 16772 mreacs 16917 cnextval 22597 taylfval 24874 iunpreima 30244 reprdifc 31797 msubvrs 32704 trpredeq1 32956 trpredeq2 32957 neibastop2 33606 voliunnfl 34817 sstotbnd2 34933 equivtotbnd 34937 totbndbnd 34948 heiborlem3 34972 eliunov2 39902 fvmptiunrelexplb0d 39907 fvmptiunrelexplb1d 39909 comptiunov2i 39929 trclrelexplem 39934 dftrcl3 39943 trclfvcom 39946 cnvtrclfv 39947 cotrcltrcl 39948 trclimalb2 39949 trclfvdecomr 39951 dfrtrcl3 39956 dfrtrcl4 39961 isomenndlem 42689 ovnval 42700 hoicvr 42707 hoicvrrex 42715 ovnlecvr 42717 ovncvrrp 42723 ovnsubaddlem1 42729 hoidmvlelem3 42756 hoidmvle 42759 ovnhoilem1 42760 ovnovollem1 42815 smflimlem3 42926 otiunsndisjX 43355 |
Copyright terms: Public domain | W3C validator |