Theorem uneq1 4102

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 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	orbi1d 917	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶)))
3		elun 4094	. . 3 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐶))
4		elun 4094	. . 3 ⊢ (𝑥 ∈ (𝐵 ∪ 𝐶) ↔ (𝑥 ∈ 𝐵 ∨ 𝑥 ∈ 𝐶))
5	2, 3, 4	3bitr4g 314	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ (𝐴 ∪ 𝐶) ↔ 𝑥 ∈ (𝐵 ∪ 𝐶)))
6	5	eqrdv 2735	1 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  uneq2  4103  uneq12  4104  uneq1i  4105  uneq1d  4108  unineq  4229  prprc1  4710  relresfld  6235  unexbOLD  7696  oarec  8491  xpider  8729  ralxpmap  8838  undifixp  8876  findcard2  9093  unxpdom  9163  enp1ilem  9182  pwfilem  9222  domunfican  9226  fin1a2lem10  10325  incexclem  15795  lcmfunsnlem  16604  ramub1lem1  16991  ramub1  16993  mreexexlem3d  17606  mreexexlem4d  17607  ipodrsima  18501  mplsubglem  21990  mretopd  23070  iscldtop  23073  nconnsubb  23401  plyval  26171  spanun  31634  difeq  32606  unelldsys  34321  isros  34331  unelros  34334  difelros  34335  rossros  34343  measun  34374  inelcarsg  34474  actfunsnf1o  34767  actfunsnrndisj  34768  mrsubvrs  35723  altopthsn  36162  rankung  36367  bj-adjg1  37369  poimirlem28  37986  islshp  39442  lshpset2N  39582  paddval  40261  nacsfix  43161  eldioph4b  43260  eldioph4i  43261  diophren  43262  clsk3nimkb  44488  isotone1  44496  fiiuncl  45517  founiiun0  45641  infxrpnf  45895  meadjun  46911  hoidmvle  47049