Theorem uneq1 4083

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 2878	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 914	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4076	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4076	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 317	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2796	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  uneq2  4084  uneq12  4085  uneq1i  4086  uneq1d  4089  unineq  4204  prprc1  4661  uniprg  4818  relresfld  6095  unexb  7451  oarec  8171  xpider  8351  ralxpmap  8443  undifixp  8481  unxpdom  8709  enp1ilem  8736  findcard2  8742  domunfican  8775  pwfilem  8802  fin1a2lem10  9820  incexclem  15183  lcmfunsnlem  15975  ramub1lem1  16352  ramub1  16354  mreexexlem3d  16909  mreexexlem4d  16910  ipodrsima  17767  mplsubglem  20672  mretopd  21697  iscldtop  21700  nconnsubb  22028  plyval  24790  spanun  29328  difeq  30289  unelldsys  31527  isros  31537  unelros  31540  difelros  31541  rossros  31549  measun  31580  inelcarsg  31679  actfunsnf1o  31985  actfunsnrndisj  31986  mrsubvrs  32882  altopthsn  33535  rankung  33740  poimirlem28  35085  islshp  36275  lshpset2N  36415  paddval  37094  nacsfix  39653  eldioph4b  39752  eldioph4i  39753  diophren  39754  clsk3nimkb  40743  isotone1  40751  fiiuncl  41699  founiiun0  41817  infxrpnf  42084  meadjun  43101  hoidmvle  43239