Theorem uneq1 4120

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  uneq2  4121  uneq12  4122  uneq1i  4123  uneq1d  4126  unineq  4247  prprc1  4725  relresfld  6237  unexbOLD  7704  oarec  8503  xpider  8738  ralxpmap  8846  undifixp  8884  findcard2  9105  unxpdom  9176  enp1ilem  9199  pwfilem  9243  domunfican  9248  fin1a2lem10  10338  incexclem  15778  lcmfunsnlem  16587  ramub1lem1  16973  ramub1  16975  mreexexlem3d  17583  mreexexlem4d  17584  ipodrsima  18476  mplsubglem  21884  mretopd  22955  iscldtop  22958  nconnsubb  23286  plyval  26074  spanun  31447  difeq  32420  unelldsys  34121  isros  34131  unelros  34134  difelros  34135  rossros  34143  measun  34174  inelcarsg  34275  actfunsnf1o  34568  actfunsnrndisj  34569  mrsubvrs  35482  altopthsn  35922  rankung  36127  bj-adjg1  37004  poimirlem28  37615  islshp  38945  lshpset2N  39085  paddval  39765  nacsfix  42673  eldioph4b  42772  eldioph4i  42773  diophren  42774  clsk3nimkb  44002  isotone1  44010  fiiuncl  45032  founiiun0  45157  infxrpnf  45415  meadjun  46433  hoidmvle  46571