Theorem uneq1 3760

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 2690	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 739	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 3753	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 3753	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 303	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2620	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 383   = wceq 1483   ∈ wcel 1990   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579

This theorem is referenced by:  uneq2  3761  uneq12  3762  uneq1i  3763  uneq1d  3766  unineq  3877  prprc1  4300  uniprg  4450  relresfld  5662  unexb  6958  oarec  7642  xpider  7818  ralxpmap  7907  undifixp  7944  unxpdom  8167  enp1ilem  8194  findcard2  8200  domunfican  8233  pwfilem  8260  fin1a2lem10  9231  incexclem  14568  lcmfunsnlem  15354  ramub1lem1  15730  ramub1  15732  mreexexlem3d  16306  mreexexlem4d  16307  ipodrsima  17165  mplsubglem  19434  mretopd  20896  iscldtop  20899  nconnsubb  21226  plyval  23949  spanun  28404  difeq  29355  unelldsys  30221  isros  30231  unelros  30234  difelros  30235  rossros  30243  measun  30274  inelcarsg  30373  actfunsnf1o  30682  actfunsnrndisj  30683  mrsubvrs  31419  altopthsn  32068  rankung  32273  poimirlem28  33437  islshp  34266  lshpset2N  34406  paddval  35084  nacsfix  37275  eldioph4b  37375  eldioph4i  37376  diophren  37377  clsk3nimkb  38338  isotone1  38346  compneOLD  38644  fiiuncl  39234  founiiun0  39377  infxrpnf  39674  meadjun  40679  hoidmvle  40814