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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151

This theorem is used by:  uneq2  4161  uneq12  4162  uneq1i  4163  uneq1d  4166  unineq  4233  prprc1  4725  relresfldOLD  6279  oarec  8570  xpider  8809  ralxpmap  8924  undifixp  8962  findcard2  9180  unxpdom  9250  enp1ilem  9269  pwfilem  9309  domunfican  9313  rankung  9873  fin1a2lem10  10487  incexclem  16005  lcmfunsnlem  16816  ramub1lem1  17204  ramub1  17206  mreexexlem3d  17820  mreexexlem4d  17821  ipodrsima  18715  mplsubglem  22306  mretopd  23410  iscldtop  23413  nconnsubb  23741  plyval  26511  spanun  32147  difeq  33114  unelldsys  34791  isros  34801  unelros  34804  difelros  34805  rossros  34813  measun  34844  inelcarsg  34943  actfunsnf1o  35233  actfunsnrndisj  35234  mrsubvrs  36287  altopthsn  36726  bj-adjg1  37956  poimirlem28  38567  islshp  40037  lshpset2N  40177  paddval  40856  nacsfix  43723  eldioph4b  43818  eldioph4i  43819  diophren  43820  clsk3nimkb  45040  isotone1  45048  fiiuncl  46082  founiiun0  46205  infxrpnf  46456  meadjun  47472  hoidmvle  47610