Theorem uneq1 4152

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 2821	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 915	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4144	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4144	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 313	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2729	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∪ cun 3942

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3949

This theorem is referenced by:  uneq2  4153  uneq12  4154  uneq1i  4155  uneq1d  4158  unineq  4273  prprc1  4762  uniprgOLD  4921  relresfld  6264  unexb  7718  oarec  8545  xpider  8765  ralxpmap  8873  undifixp  8911  findcard2  9147  pwfilem  9160  unxpdom  9236  enp1ilem  9261  findcard2OLD  9267  domunfican  9303  pwfilemOLD  9329  fin1a2lem10  10386  incexclem  15764  lcmfunsnlem  16560  ramub1lem1  16941  ramub1  16943  mreexexlem3d  17572  mreexexlem4d  17573  ipodrsima  18476  mplsubglem  21487  mretopd  22525  iscldtop  22528  nconnsubb  22856  plyval  25636  spanun  30661  difeq  31620  unelldsys  32987  isros  32997  unelros  33000  difelros  33001  rossros  33009  measun  33040  inelcarsg  33141  actfunsnf1o  33447  actfunsnrndisj  33448  mrsubvrs  34344  altopthsn  34763  rankung  34968  bj-adjg1  35728  poimirlem28  36320  islshp  37654  lshpset2N  37794  paddval  38474  nacsfix  41221  eldioph4b  41320  eldioph4i  41321  diophren  41322  clsk3nimkb  42562  isotone1  42570  fiiuncl  43523  founiiun0  43659  infxrpnf  43929  meadjun  44951  hoidmvle  45089