Theorem uneq1 4141

Description: Equality theorem for the union of two classes. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
uneq1	⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Proof of Theorem uneq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq2 2824	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 916	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4133	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4133	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 314	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2734	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936

This theorem is referenced by:  uneq2  4142  uneq12  4143  uneq1i  4144  uneq1d  4147  unineq  4268  prprc1  4746  relresfld  6270  unexbOLD  7747  oarec  8579  xpider  8807  ralxpmap  8915  undifixp  8953  findcard2  9183  unxpdom  9266  enp1ilem  9289  pwfilem  9333  domunfican  9338  fin1a2lem10  10428  incexclem  15857  lcmfunsnlem  16665  ramub1lem1  17051  ramub1  17053  mreexexlem3d  17663  mreexexlem4d  17664  ipodrsima  18556  mplsubglem  21964  mretopd  23035  iscldtop  23038  nconnsubb  23366  plyval  26155  spanun  31531  difeq  32504  unelldsys  34194  isros  34204  unelros  34207  difelros  34208  rossros  34216  measun  34247  inelcarsg  34348  actfunsnf1o  34641  actfunsnrndisj  34642  mrsubvrs  35549  altopthsn  35984  rankung  36189  bj-adjg1  37066  poimirlem28  37677  islshp  39002  lshpset2N  39142  paddval  39822  nacsfix  42702  eldioph4b  42801  eldioph4i  42802  diophren  42803  clsk3nimkb  44031  isotone1  44039  fiiuncl  45056  founiiun0  45181  infxrpnf  45440  meadjun  46458  hoidmvle  46596