Theorem uneq1 4108

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

Syntax hints:   → wi 4   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  uneq2  4109  uneq12  4110  uneq1i  4111  uneq1d  4114  unineq  4235  prprc1  4715  relresfld  6223  unexbOLD  7681  oarec  8477  xpider  8712  ralxpmap  8820  undifixp  8858  findcard2  9074  unxpdom  9143  enp1ilem  9162  pwfilem  9202  domunfican  9206  fin1a2lem10  10300  incexclem  15743  lcmfunsnlem  16552  ramub1lem1  16938  ramub1  16940  mreexexlem3d  17552  mreexexlem4d  17553  ipodrsima  18447  mplsubglem  21936  mretopd  23007  iscldtop  23010  nconnsubb  23338  plyval  26125  spanun  31525  difeq  32498  unelldsys  34171  isros  34181  unelros  34184  difelros  34185  rossros  34193  measun  34224  inelcarsg  34324  actfunsnf1o  34617  actfunsnrndisj  34618  mrsubvrs  35566  altopthsn  36003  rankung  36208  bj-adjg1  37085  poimirlem28  37696  islshp  39026  lshpset2N  39166  paddval  39845  nacsfix  42753  eldioph4b  42852  eldioph4i  42853  diophren  42854  clsk3nimkb  44081  isotone1  44089  fiiuncl  45110  founiiun0  45235  infxrpnf  45492  meadjun  46508  hoidmvle  46646