Theorem cnvun 6164

Description: The converse of a union is the union of converses. Theorem 16 of [Suppes] p. 62. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
cnvun	⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)

Proof of Theorem cnvun

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-cnv 5696	. . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
2		unopab 5229	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
3		brun 5198	. . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4	3	opabbii 5214	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
5	2, 4	eqtr4i 2765	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
6	1, 5	eqtr4i 2765	. 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
7		df-cnv 5696	. . 3 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
8		df-cnv 5696	. . 3 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
9	7, 8	uneq12i 4175	. 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
10	6, 9	eqtr4i 2765	1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)

Syntax hints:   ∨ wo 847   = wceq 1536   ∪ cun 3960   class class class wbr 5147  {copab 5209  ^◡ccnv 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-br 5148  df-opab 5210  df-cnv 5696

This theorem is referenced by:  rnun  6167  funcnvpr  6629  funcnvtp  6630  funcnvqp  6631  f1oun  6867  f1oprswap  6892  suppun  8207  sbthlem8  9128  domss2  9174  cnvfi  9214  1sdomOLD  9282  fsuppun  9424  fpwwe2lem12  10679  trclublem  15030  mbfres2  25693  ex-cnv  30465  suppun2  32698  cnvprop  32710  padct  32736  cycpmconjslem2  33157  eulerpartlemt  34352  mthmpps  35566  clcnvlem  43612  frege131d  43753