Theorem iuneq2d 4950

Description: Equality deduction for indexed union. (Contributed by Drahflow, 22-Oct-2015.)

Hypothesis

Ref	Expression
iuneq2d.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2d	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2d

Step	Hyp	Ref	Expression
1		iuneq2d.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
2	1	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	iuneq2dv 4945	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∪ ciun 4921

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-in 3945  df-ss 3954  df-iun 4923

This theorem is referenced by:  iununi  5023  oelim2  8223  ituniiun  9846  dfrtrclrec2  14418  rtrclreclem1  14419  rtrclreclem2  14420  rtrclreclem4  14422  imasval  16786  mreacs  16931  cnextval  22671  taylfval  24949  iunpreima  30318  reprdifc  31900  msubvrs  32809  trpredeq1  33061  trpredeq2  33062  neibastop2  33711  voliunnfl  34938  sstotbnd2  35054  equivtotbnd  35058  totbndbnd  35069  heiborlem3  35093  eliunov2  40031  fvmptiunrelexplb0d  40036  fvmptiunrelexplb1d  40038  comptiunov2i  40058  trclrelexplem  40063  dftrcl3  40072  trclfvcom  40075  cnvtrclfv  40076  cotrcltrcl  40077  trclimalb2  40078  trclfvdecomr  40080  dfrtrcl3  40085  dfrtrcl4  40090  isomenndlem  42819  ovnval  42830  hoicvr  42837  hoicvrrex  42845  ovnlecvr  42847  ovncvrrp  42853  ovnsubaddlem1  42859  hoidmvlelem3  42886  hoidmvle  42889  ovnhoilem1  42890  ovnovollem1  42945  smflimlem3  43056  otiunsndisjX  43485