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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ∪ cun 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  uneq2  4116  uneq12  4117  uneq1i  4118  uneq1d  4121  unineq  4241  prprc1  4733  relresfldOLD  6281  oarec  8553  xpider  8792  ralxpmap  8900  undifixp  8938  findcard2  9156  unxpdom  9226  enp1ilem  9245  pwfilem  9284  domunfican  9288  fin1a2lem10  10408  incexclem  15913  lcmfunsnlem  16721  ramub1lem1  17108  ramub1  17110  mreexexlem3d  17724  mreexexlem4d  17725  ipodrsima  18619  mplsubglem  22198  mretopd  23299  iscldtop  23302  nconnsubb  23630  plyval  26401  spanun  31968  difeq  32935  unelldsys  34613  isros  34623  unelros  34626  difelros  34627  rossros  34635  measun  34666  inelcarsg  34766  actfunsnf1o  35056  actfunsnrndisj  35057  mrsubvrs  36051  altopthsn  36490  rankung  36695  bj-adjg1  37736  poimirlem28  38356  islshp  39811  lshpset2N  39951  paddval  40630  nacsfix  43501  eldioph4b  43596  eldioph4i  43597  diophren  43598  clsk3nimkb  44824  isotone1  44832  fiiuncl  45843  founiiun0  45966  infxrpnf  46218  meadjun  47234  hoidmvle  47372