Theorem uneq1 4171

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1537   ∈ wcel 2106   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968

This theorem is referenced by:  uneq2  4172  uneq12  4173  uneq1i  4174  uneq1d  4177  unineq  4294  prprc1  4770  relresfld  6298  unexbOLD  7767  oarec  8599  xpider  8827  ralxpmap  8935  undifixp  8973  findcard2  9203  unxpdom  9287  enp1ilem  9310  pwfilem  9354  domunfican  9359  fin1a2lem10  10447  incexclem  15869  lcmfunsnlem  16675  ramub1lem1  17060  ramub1  17062  mreexexlem3d  17691  mreexexlem4d  17692  ipodrsima  18599  mplsubglem  22037  mretopd  23116  iscldtop  23119  nconnsubb  23447  plyval  26247  spanun  31574  difeq  32546  unelldsys  34139  isros  34149  unelros  34152  difelros  34153  rossros  34161  measun  34192  inelcarsg  34293  actfunsnf1o  34598  actfunsnrndisj  34599  mrsubvrs  35507  altopthsn  35943  rankung  36148  bj-adjg1  37026  poimirlem28  37635  islshp  38961  lshpset2N  39101  paddval  39781  nacsfix  42700  eldioph4b  42799  eldioph4i  42800  diophren  42801  clsk3nimkb  44030  isotone1  44038  fiiuncl  45005  founiiun0  45133  infxrpnf  45396  meadjun  46418  hoidmvle  46556