Theorem uneq1 4091

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 2828	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 922	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4083	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4083	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 315	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2737	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∨ wo 853   = wceq 1547   ∈ wcel 2119   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  uneq2  4092  uneq12  4093  uneq1i  4094  uneq1d  4097  unineq  4216  prprc1  4697  relresfld  6227  unexbOLD  7691  oarec  8487  xpider  8725  ralxpmap  8834  undifixp  8872  findcard2  9089  unxpdom  9159  enp1ilem  9178  pwfilem  9218  domunfican  9222  fin1a2lem10  10322  incexclem  15792  lcmfunsnlem  16601  ramub1lem1  16988  ramub1  16990  mreexexlem3d  17603  mreexexlem4d  17604  ipodrsima  18498  mplsubglem  21973  mretopd  23075  iscldtop  23078  nconnsubb  23406  plyval  26176  spanun  31634  difeq  32606  unelldsys  34342  isros  34352  unelros  34355  difelros  34356  rossros  34364  measun  34395  inelcarsg  34495  actfunsnf1o  34788  actfunsnrndisj  34789  mrsubvrs  35750  altopthsn  36189  rankung  36394  bj-adjg1  37396  poimirlem28  38015  islshp  39471  lshpset2N  39611  paddval  40290  nacsfix  43161  eldioph4b  43256  eldioph4i  43257  diophren  43258  clsk3nimkb  44484  isotone1  44492  fiiuncl  45513  founiiun0  45637  infxrpnf  45889  meadjun  46905  hoidmvle  47043