Theorem uneq1 4124

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  uneq2  4125  uneq12  4126  uneq1i  4127  uneq1d  4130  unineq  4251  prprc1  4729  relresfld  6249  unexbOLD  7724  oarec  8526  xpider  8761  ralxpmap  8869  undifixp  8907  findcard2  9128  unxpdom  9200  enp1ilem  9223  pwfilem  9267  domunfican  9272  fin1a2lem10  10362  incexclem  15802  lcmfunsnlem  16611  ramub1lem1  16997  ramub1  16999  mreexexlem3d  17607  mreexexlem4d  17608  ipodrsima  18500  mplsubglem  21908  mretopd  22979  iscldtop  22982  nconnsubb  23310  plyval  26098  spanun  31474  difeq  32447  unelldsys  34148  isros  34158  unelros  34161  difelros  34162  rossros  34170  measun  34201  inelcarsg  34302  actfunsnf1o  34595  actfunsnrndisj  34596  mrsubvrs  35509  altopthsn  35949  rankung  36154  bj-adjg1  37031  poimirlem28  37642  islshp  38972  lshpset2N  39112  paddval  39792  nacsfix  42700  eldioph4b  42799  eldioph4i  42800  diophren  42801  clsk3nimkb  44029  isotone1  44037  fiiuncl  45059  founiiun0  45184  infxrpnf  45442  meadjun  46460  hoidmvle  46598