Theorem uneq1 4120

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 2817	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 916	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4112	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4112	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 314	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2727	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  uneq2  4121  uneq12  4122  uneq1i  4123  uneq1d  4126  unineq  4247  prprc1  4725  relresfld  6237  unexbOLD  7704  oarec  8503  xpider  8738  ralxpmap  8846  undifixp  8884  findcard2  9105  unxpdom  9176  enp1ilem  9199  pwfilem  9243  domunfican  9248  fin1a2lem10  10338  incexclem  15778  lcmfunsnlem  16587  ramub1lem1  16973  ramub1  16975  mreexexlem3d  17587  mreexexlem4d  17588  ipodrsima  18482  mplsubglem  21941  mretopd  23012  iscldtop  23015  nconnsubb  23343  plyval  26131  spanun  31524  difeq  32497  unelldsys  34141  isros  34151  unelros  34154  difelros  34155  rossros  34163  measun  34194  inelcarsg  34295  actfunsnf1o  34588  actfunsnrndisj  34589  mrsubvrs  35502  altopthsn  35942  rankung  36147  bj-adjg1  37024  poimirlem28  37635  islshp  38965  lshpset2N  39105  paddval  39785  nacsfix  42693  eldioph4b  42792  eldioph4i  42793  diophren  42794  clsk3nimkb  44022  isotone1  44030  fiiuncl  45052  founiiun0  45177  infxrpnf  45435  meadjun  46453  hoidmvle  46591