Theorem uneq1 4111

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  uneq2  4112  uneq12  4113  uneq1i  4114  uneq1d  4117  unineq  4238  prprc1  4720  relresfld  6232  unexbOLD  7691  oarec  8487  xpider  8723  ralxpmap  8832  undifixp  8870  findcard2  9087  unxpdom  9157  enp1ilem  9176  pwfilem  9216  domunfican  9220  fin1a2lem10  10317  incexclem  15757  lcmfunsnlem  16566  ramub1lem1  16952  ramub1  16954  mreexexlem3d  17567  mreexexlem4d  17568  ipodrsima  18462  mplsubglem  21952  mretopd  23034  iscldtop  23037  nconnsubb  23365  plyval  26152  spanun  31569  difeq  32542  unelldsys  34264  isros  34274  unelros  34277  difelros  34278  rossros  34286  measun  34317  inelcarsg  34417  actfunsnf1o  34710  actfunsnrndisj  34711  mrsubvrs  35665  altopthsn  36104  rankung  36309  bj-adjg1  37187  poimirlem28  37788  islshp  39178  lshpset2N  39318  paddval  39997  nacsfix  42896  eldioph4b  42995  eldioph4i  42996  diophren  42997  clsk3nimkb  44223  isotone1  44231  fiiuncl  45252  founiiun0  45376  infxrpnf  45632  meadjun  46648  hoidmvle  46786