Theorem uneq1 4115

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

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

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 3444  df-un 3908

This theorem is referenced by:  uneq2  4116  uneq12  4117  uneq1i  4118  uneq1d  4121  unineq  4242  prprc1  4724  relresfld  6242  unexbOLD  7703  oarec  8499  xpider  8737  ralxpmap  8846  undifixp  8884  findcard2  9101  unxpdom  9171  enp1ilem  9190  pwfilem  9230  domunfican  9234  fin1a2lem10  10331  incexclem  15771  lcmfunsnlem  16580  ramub1lem1  16966  ramub1  16968  mreexexlem3d  17581  mreexexlem4d  17582  ipodrsima  18476  mplsubglem  21966  mretopd  23048  iscldtop  23051  nconnsubb  23379  plyval  26166  spanun  31633  difeq  32605  unelldsys  34336  isros  34346  unelros  34349  difelros  34350  rossros  34358  measun  34389  inelcarsg  34489  actfunsnf1o  34782  actfunsnrndisj  34783  mrsubvrs  35738  altopthsn  36177  rankung  36382  bj-adjg1  37291  poimirlem28  37899  islshp  39355  lshpset2N  39495  paddval  40174  nacsfix  43069  eldioph4b  43168  eldioph4i  43169  diophren  43170  clsk3nimkb  44396  isotone1  44404  fiiuncl  45425  founiiun0  45549  infxrpnf  45804  meadjun  46820  hoidmvle  46958