Theorem uneq1 4113

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  uneq2  4114  uneq12  4115  uneq1i  4116  uneq1d  4119  unineq  4240  prprc1  4722  relresfld  6234  unexbOLD  7693  oarec  8489  xpider  8725  ralxpmap  8834  undifixp  8872  findcard2  9089  unxpdom  9159  enp1ilem  9178  pwfilem  9218  domunfican  9222  fin1a2lem10  10319  incexclem  15759  lcmfunsnlem  16568  ramub1lem1  16954  ramub1  16956  mreexexlem3d  17569  mreexexlem4d  17570  ipodrsima  18464  mplsubglem  21954  mretopd  23036  iscldtop  23039  nconnsubb  23367  plyval  26154  spanun  31620  difeq  32593  unelldsys  34315  isros  34325  unelros  34328  difelros  34329  rossros  34337  measun  34368  inelcarsg  34468  actfunsnf1o  34761  actfunsnrndisj  34762  mrsubvrs  35716  altopthsn  36155  rankung  36360  bj-adjg1  37244  poimirlem28  37849  islshp  39239  lshpset2N  39379  paddval  40058  nacsfix  42954  eldioph4b  43053  eldioph4i  43054  diophren  43055  clsk3nimkb  44281  isotone1  44289  fiiuncl  45310  founiiun0  45434  infxrpnf  45690  meadjun  46706  hoidmvle  46844