Theorem uneq1 4159

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861   = wceq 1569   ∈ wcel 2144   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150

This theorem is used by:  uneq2  4160  uneq12  4161  uneq1i  4162  uneq1d  4165  unineq  4232  prprc1  4722  relresfldOLD  6282  oarec  8577  xpider  8816  ralxpmap  8931  undifixp  8969  findcard2  9187  unxpdom  9257  enp1ilem  9276  pwfilem  9316  domunfican  9320  rankung  9880  fin1a2lem10  10494  incexclem  16014  lcmfunsnlem  16825  ramub1lem1  17213  ramub1  17215  mreexexlem3d  17829  mreexexlem4d  17830  ipodrsima  18724  mplsubglem  22315  mretopd  23419  iscldtop  23422  nconnsubb  23750  plyval  26520  spanun  32156  difeq  33165  unelldsys  34841  isros  34851  unelros  34854  difelros  34855  rossros  34863  measun  34894  inelcarsg  34993  actfunsnf1o  35283  actfunsnrndisj  35284  maxssj0  35949  mrsubvrs  36377  altopthsn  36822  bj-adjg1  38052  poimirlem28  38675  islshp  40145  lshpset2N  40285  paddval  40964  nacsfix  43832  eldioph4b  43927  eldioph4i  43928  diophren  43929  clsk3nimkb  45149  isotone1  45157  fiiuncl  46190  founiiun0  46313  infxrpnf  46564  meadjun  47580  hoidmvle  47718