Theorem uneq1 4127

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  uneq2  4128  uneq12  4129  uneq1i  4130  uneq1d  4133  unineq  4254  prprc1  4732  relresfld  6252  unexbOLD  7727  oarec  8529  xpider  8764  ralxpmap  8872  undifixp  8910  findcard2  9134  unxpdom  9207  enp1ilem  9230  pwfilem  9274  domunfican  9279  fin1a2lem10  10369  incexclem  15809  lcmfunsnlem  16618  ramub1lem1  17004  ramub1  17006  mreexexlem3d  17614  mreexexlem4d  17615  ipodrsima  18507  mplsubglem  21915  mretopd  22986  iscldtop  22989  nconnsubb  23317  plyval  26105  spanun  31481  difeq  32454  unelldsys  34155  isros  34165  unelros  34168  difelros  34169  rossros  34177  measun  34208  inelcarsg  34309  actfunsnf1o  34602  actfunsnrndisj  34603  mrsubvrs  35516  altopthsn  35956  rankung  36161  bj-adjg1  37038  poimirlem28  37649  islshp  38979  lshpset2N  39119  paddval  39799  nacsfix  42707  eldioph4b  42806  eldioph4i  42807  diophren  42808  clsk3nimkb  44036  isotone1  44044  fiiuncl  45066  founiiun0  45191  infxrpnf  45449  meadjun  46467  hoidmvle  46605