Theorem uneq1 4123

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

Syntax hints:   → wi 4   ∨ wo 860   = wceq 1567   ∈ wcel 2149   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918

This theorem is referenced by:  uneq2  4124  uneq12  4125  uneq1i  4126  uneq1d  4129  unineq  4249  prprc1  4736  relresfld  6278  unexbOLD  7746  oarec  8546  xpider  8785  ralxpmap  8893  undifixp  8931  findcard2  9148  unxpdom  9218  enp1ilem  9237  pwfilem  9276  domunfican  9280  fin1a2lem10  10392  incexclem  15889  lcmfunsnlem  16698  ramub1lem1  17085  ramub1  17087  mreexexlem3d  17701  mreexexlem4d  17702  ipodrsima  18596  mplsubglem  22116  mretopd  23217  iscldtop  23220  nconnsubb  23548  plyval  26318  spanun  31837  difeq  32804  unelldsys  34492  isros  34502  unelros  34505  difelros  34506  rossros  34514  measun  34545  inelcarsg  34645  actfunsnf1o  34935  actfunsnrndisj  34936  mrsubvrs  35912  altopthsn  36351  rankung  36556  bj-adjg1  37566  poimirlem28  38186  islshp  39642  lshpset2N  39782  paddval  40461  nacsfix  43334  eldioph4b  43429  eldioph4i  43430  diophren  43431  clsk3nimkb  44657  isotone1  44665  fiiuncl  45676  founiiun0  45799  infxrpnf  46051  meadjun  47067  hoidmvle  47205