Theorem uneq1 4114

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 2851	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 927	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4106	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4106	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 316	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2760	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 858   = wceq 1560   ∈ wcel 2142   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  uneq2  4115  uneq12  4116  uneq1i  4117  uneq1d  4120  unineq  4240  prprc1  4724  relresfld  6263  unexbOLD  7731  oarec  8531  xpider  8770  ralxpmap  8878  undifixp  8916  findcard2  9133  unxpdom  9203  enp1ilem  9222  pwfilem  9262  domunfican  9266  fin1a2lem10  10366  incexclem  15866  lcmfunsnlem  16675  ramub1lem1  17062  ramub1  17064  mreexexlem3d  17678  mreexexlem4d  17679  ipodrsima  18573  mplsubglem  22047  mretopd  23149  iscldtop  23152  nconnsubb  23480  plyval  26250  spanun  31745  difeq  32714  unelldsys  34452  isros  34462  unelros  34465  difelros  34466  rossros  34474  measun  34505  inelcarsg  34605  actfunsnf1o  34895  actfunsnrndisj  34896  mrsubvrs  35869  altopthsn  36308  rankung  36513  bj-adjg1  37525  poimirlem28  38144  islshp  39600  lshpset2N  39740  paddval  40419  nacsfix  43290  eldioph4b  43385  eldioph4i  43386  diophren  43387  clsk3nimkb  44613  isotone1  44621  fiiuncl  45642  founiiun0  45765  infxrpnf  46017  meadjun  47033  hoidmvle  47171