Theorem uneq1 4184

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  uneq2  4185  uneq12  4186  uneq1i  4187  uneq1d  4190  unineq  4307  prprc1  4790  relresfld  6307  unexbOLD  7783  oarec  8618  xpider  8846  ralxpmap  8954  undifixp  8992  findcard2  9230  unxpdom  9316  enp1ilem  9340  pwfilem  9384  domunfican  9389  pwfilemOLD  9416  fin1a2lem10  10478  incexclem  15884  lcmfunsnlem  16688  ramub1lem1  17073  ramub1  17075  mreexexlem3d  17704  mreexexlem4d  17705  ipodrsima  18611  mplsubglem  22042  mretopd  23121  iscldtop  23124  nconnsubb  23452  plyval  26252  spanun  31577  difeq  32548  unelldsys  34122  isros  34132  unelros  34135  difelros  34136  rossros  34144  measun  34175  inelcarsg  34276  actfunsnf1o  34581  actfunsnrndisj  34582  mrsubvrs  35490  altopthsn  35925  rankung  36130  bj-adjg1  37009  poimirlem28  37608  islshp  38935  lshpset2N  39075  paddval  39755  nacsfix  42668  eldioph4b  42767  eldioph4i  42768  diophren  42769  clsk3nimkb  44002  isotone1  44010  fiiuncl  44967  founiiun0  45097  infxrpnf  45361  meadjun  46383  hoidmvle  46521