Theorem uneq1 4160

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1539   ∈ wcel 2107   ∪ cun 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955

This theorem is referenced by:  uneq2  4161  uneq12  4162  uneq1i  4163  uneq1d  4166  unineq  4287  prprc1  4764  relresfld  6295  unexbOLD  7769  oarec  8601  xpider  8829  ralxpmap  8937  undifixp  8975  findcard2  9205  unxpdom  9290  enp1ilem  9313  pwfilem  9357  domunfican  9362  fin1a2lem10  10450  incexclem  15873  lcmfunsnlem  16679  ramub1lem1  17065  ramub1  17067  mreexexlem3d  17690  mreexexlem4d  17691  ipodrsima  18587  mplsubglem  22020  mretopd  23101  iscldtop  23104  nconnsubb  23432  plyval  26233  spanun  31565  difeq  32538  unelldsys  34160  isros  34170  unelros  34173  difelros  34174  rossros  34182  measun  34213  inelcarsg  34314  actfunsnf1o  34620  actfunsnrndisj  34621  mrsubvrs  35528  altopthsn  35963  rankung  36168  bj-adjg1  37045  poimirlem28  37656  islshp  38981  lshpset2N  39121  paddval  39801  nacsfix  42728  eldioph4b  42827  eldioph4i  42828  diophren  42829  clsk3nimkb  44058  isotone1  44066  fiiuncl  45075  founiiun0  45200  infxrpnf  45462  meadjun  46482  hoidmvle  46620