Theorem uneq1 4121

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

Syntax hints:   → wi 4   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918

This theorem is referenced by:  uneq2  4122  uneq12  4123  uneq1i  4124  uneq1d  4127  unineq  4242  prprc1  4731  uniprgOLD  4890  relresfld  6233  unexb  7687  oarec  8514  xpider  8734  ralxpmap  8841  undifixp  8879  findcard2  9115  pwfilem  9128  unxpdom  9204  enp1ilem  9229  findcard2OLD  9235  domunfican  9271  pwfilemOLD  9297  fin1a2lem10  10354  incexclem  15732  lcmfunsnlem  16528  ramub1lem1  16909  ramub1  16911  mreexexlem3d  17540  mreexexlem4d  17541  ipodrsima  18444  mplsubglem  21442  mretopd  22480  iscldtop  22483  nconnsubb  22811  plyval  25591  spanun  30550  difeq  31509  unelldsys  32846  isros  32856  unelros  32859  difelros  32860  rossros  32868  measun  32899  inelcarsg  33000  actfunsnf1o  33306  actfunsnrndisj  33307  mrsubvrs  34203  altopthsn  34622  rankung  34827  bj-adjg1  35587  poimirlem28  36179  islshp  37514  lshpset2N  37654  paddval  38334  nacsfix  41093  eldioph4b  41192  eldioph4i  41193  diophren  41194  clsk3nimkb  42434  isotone1  42442  fiiuncl  43395  founiiun0  43531  infxrpnf  43801  meadjun  44823  hoidmvle  44961