Theorem uneq1 4108

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 2849	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 930	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4100	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4100	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 317	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2758	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  uneq2  4109  uneq12  4110  uneq1i  4111  uneq1d  4114  unineq  4234  prprc1  4726  relresfldOLD  6274  oarec  8549  xpider  8788  ralxpmap  8903  undifixp  8941  findcard2  9159  unxpdom  9229  enp1ilem  9248  pwfilem  9287  domunfican  9291  fin1a2lem10  10411  incexclem  15925  lcmfunsnlem  16731  ramub1lem1  17118  ramub1  17120  mreexexlem3d  17734  mreexexlem4d  17735  ipodrsima  18629  mplsubglem  22213  mretopd  23317  iscldtop  23320  nconnsubb  23648  plyval  26418  spanun  32026  difeq  32993  unelldsys  34669  isros  34679  unelros  34682  difelros  34683  rossros  34691  measun  34722  inelcarsg  34822  actfunsnf1o  35112  actfunsnrndisj  35113  mrsubvrs  36101  altopthsn  36541  rankung  36746  bj-adjg1  37787  poimirlem28  38397  islshp  39852  lshpset2N  39992  paddval  40671  nacsfix  43557  eldioph4b  43652  eldioph4i  43653  diophren  43654  clsk3nimkb  44880  isotone1  44888  fiiuncl  45899  founiiun0  46022  infxrpnf  46274  meadjun  47290  hoidmvle  47428