Theorem uneq1 4102

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

Syntax hints:   → wi 4   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3888

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  uneq2  4103  uneq12  4104  uneq1i  4105  uneq1d  4108  unineq  4229  prprc1  4710  relresfld  6232  unexbOLD  7693  oarec  8488  xpider  8726  ralxpmap  8835  undifixp  8873  findcard2  9090  unxpdom  9160  enp1ilem  9179  pwfilem  9219  domunfican  9223  fin1a2lem10  10320  incexclem  15760  lcmfunsnlem  16569  ramub1lem1  16955  ramub1  16957  mreexexlem3d  17570  mreexexlem4d  17571  ipodrsima  18465  mplsubglem  21955  mretopd  23035  iscldtop  23038  nconnsubb  23366  plyval  26139  spanun  31605  difeq  32577  unelldsys  34308  isros  34318  unelros  34321  difelros  34322  rossros  34330  measun  34361  inelcarsg  34461  actfunsnf1o  34754  actfunsnrndisj  34755  mrsubvrs  35710  altopthsn  36149  rankung  36354  bj-adjg1  37348  poimirlem28  37960  islshp  39416  lshpset2N  39556  paddval  40235  nacsfix  43143  eldioph4b  43242  eldioph4i  43243  diophren  43244  clsk3nimkb  44470  isotone1  44478  fiiuncl  45499  founiiun0  45623  infxrpnf  45878  meadjun  46894  hoidmvle  47032