Theorem uneq1 4112

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

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

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 3438  df-un 3908

This theorem is referenced by:  uneq2  4113  uneq12  4114  uneq1i  4115  uneq1d  4118  unineq  4239  prprc1  4717  relresfld  6224  unexbOLD  7684  oarec  8480  xpider  8715  ralxpmap  8823  undifixp  8861  findcard2  9078  unxpdom  9148  enp1ilem  9167  pwfilem  9207  domunfican  9211  fin1a2lem10  10303  incexclem  15743  lcmfunsnlem  16552  ramub1lem1  16938  ramub1  16940  mreexexlem3d  17552  mreexexlem4d  17553  ipodrsima  18447  mplsubglem  21906  mretopd  22977  iscldtop  22980  nconnsubb  23308  plyval  26096  spanun  31489  difeq  32462  unelldsys  34125  isros  34135  unelros  34138  difelros  34139  rossros  34147  measun  34178  inelcarsg  34279  actfunsnf1o  34572  actfunsnrndisj  34573  mrsubvrs  35495  altopthsn  35935  rankung  36140  bj-adjg1  37017  poimirlem28  37628  islshp  38958  lshpset2N  39098  paddval  39777  nacsfix  42685  eldioph4b  42784  eldioph4i  42785  diophren  42786  clsk3nimkb  44013  isotone1  44021  fiiuncl  45043  founiiun0  45168  infxrpnf  45425  meadjun  46443  hoidmvle  46581