Theorem uneq1 4157

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

Syntax hints:   → wi 4   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ∪ cun 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3954

This theorem is referenced by:  uneq2  4158  uneq12  4159  uneq1i  4160  uneq1d  4163  unineq  4278  prprc1  4770  uniprgOLD  4929  relresfld  6276  unexb  7739  oarec  8566  xpider  8786  ralxpmap  8894  undifixp  8932  findcard2  9168  pwfilem  9181  unxpdom  9257  enp1ilem  9282  findcard2OLD  9288  domunfican  9324  pwfilemOLD  9350  fin1a2lem10  10408  incexclem  15788  lcmfunsnlem  16584  ramub1lem1  16965  ramub1  16967  mreexexlem3d  17596  mreexexlem4d  17597  ipodrsima  18500  mplsubglem  21779  mretopd  22818  iscldtop  22821  nconnsubb  23149  plyval  25941  spanun  31063  difeq  32021  unelldsys  33452  isros  33462  unelros  33465  difelros  33466  rossros  33474  measun  33505  inelcarsg  33606  actfunsnf1o  33912  actfunsnrndisj  33913  mrsubvrs  34809  altopthsn  35235  rankung  35440  bj-adjg1  36229  poimirlem28  36821  islshp  38154  lshpset2N  38294  paddval  38974  nacsfix  41754  eldioph4b  41853  eldioph4i  41854  diophren  41855  clsk3nimkb  43095  isotone1  43103  fiiuncl  44055  founiiun0  44189  infxrpnf  44456  meadjun  45478  hoidmvle  45616