Theorem uneq1 4056

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

Syntax hints:   → wi 4   ∨ wo 846   = wceq 1542   ∈ wcel 2114   ∪ cun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858

This theorem is referenced by:  uneq2  4057  uneq12  4058  uneq1i  4059  uneq1d  4062  unineq  4178  prprc1  4666  uniprgOLD  4826  relresfld  6118  unexb  7502  oarec  8232  xpider  8412  ralxpmap  8519  undifixp  8557  findcard2  8776  pwfilem  8788  unxpdom  8817  enp1ilem  8842  findcard2OLD  8847  domunfican  8878  pwfilemOLD  8904  fin1a2lem10  9922  incexclem  15297  lcmfunsnlem  16095  ramub1lem1  16475  ramub1  16477  mreexexlem3d  17033  mreexexlem4d  17034  ipodrsima  17904  mplsubglem  20828  mretopd  21856  iscldtop  21859  nconnsubb  22187  plyval  24955  spanun  29493  difeq  30452  unelldsys  31709  isros  31719  unelros  31722  difelros  31723  rossros  31731  measun  31762  inelcarsg  31861  actfunsnf1o  32167  actfunsnrndisj  32168  mrsubvrs  33068  altopthsn  33919  rankung  34124  poimirlem28  35461  islshp  36649  lshpset2N  36789  paddval  37468  nacsfix  40147  eldioph4b  40246  eldioph4i  40247  diophren  40248  clsk3nimkb  41237  isotone1  41245  fiiuncl  42192  founiiun0  42307  infxrpnf  42566  meadjun  43583  hoidmvle  43721