Theorem uneq1 4101

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  uneq2  4102  uneq12  4103  uneq1i  4104  uneq1d  4107  unineq  4228  prprc1  4709  relresfld  6240  unexbOLD  7702  oarec  8497  xpider  8735  ralxpmap  8844  undifixp  8882  findcard2  9099  unxpdom  9169  enp1ilem  9188  pwfilem  9228  domunfican  9232  fin1a2lem10  10331  incexclem  15801  lcmfunsnlem  16610  ramub1lem1  16997  ramub1  16999  mreexexlem3d  17612  mreexexlem4d  17613  ipodrsima  18507  mplsubglem  21977  mretopd  23057  iscldtop  23060  nconnsubb  23388  plyval  26158  spanun  31616  difeq  32588  unelldsys  34302  isros  34312  unelros  34315  difelros  34316  rossros  34324  measun  34355  inelcarsg  34455  actfunsnf1o  34748  actfunsnrndisj  34749  mrsubvrs  35704  altopthsn  36143  rankung  36348  bj-adjg1  37350  poimirlem28  37969  islshp  39425  lshpset2N  39565  paddval  40244  nacsfix  43144  eldioph4b  43239  eldioph4i  43240  diophren  43241  clsk3nimkb  44467  isotone1  44475  fiiuncl  45496  founiiun0  45620  infxrpnf  45874  meadjun  46890  hoidmvle  47028