Theorem uneq1 4086

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 2827	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 913	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4079	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4079	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 313	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2736	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  uneq2  4087  uneq12  4088  uneq1i  4089  uneq1d  4092  unineq  4208  prprc1  4698  uniprgOLD  4856  relresfld  6168  unexb  7576  oarec  8355  xpider  8535  ralxpmap  8642  undifixp  8680  findcard2  8909  pwfilem  8922  unxpdom  8959  enp1ilem  8981  findcard2OLD  8986  domunfican  9017  pwfilemOLD  9043  fin1a2lem10  10096  incexclem  15476  lcmfunsnlem  16274  ramub1lem1  16655  ramub1  16657  mreexexlem3d  17272  mreexexlem4d  17273  ipodrsima  18174  mplsubglem  21115  mretopd  22151  iscldtop  22154  nconnsubb  22482  plyval  25259  spanun  29808  difeq  30766  unelldsys  32026  isros  32036  unelros  32039  difelros  32040  rossros  32048  measun  32079  inelcarsg  32178  actfunsnf1o  32484  actfunsnrndisj  32485  mrsubvrs  33384  altopthsn  34190  rankung  34395  poimirlem28  35732  islshp  36920  lshpset2N  37060  paddval  37739  nacsfix  40450  eldioph4b  40549  eldioph4i  40550  diophren  40551  clsk3nimkb  41539  isotone1  41547  fiiuncl  42502  founiiun0  42617  infxrpnf  42876  meadjun  43890  hoidmvle  44028