Theorem cnvun 6162

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 5693	. . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
2		unopab 5224	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
3		brun 5194	. . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4	3	opabbii 5210	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
5	2, 4	eqtr4i 2768	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
6	1, 5	eqtr4i 2768	. 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
7		df-cnv 5693	. . 3 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
8		df-cnv 5693	. . 3 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
9	7, 8	uneq12i 4166	. 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
10	6, 9	eqtr4i 2768	1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)

Syntax hints:   ∨ wo 848   = wceq 1540   ∪ cun 3949   class class class wbr 5143  {copab 5205  ^◡ccnv 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-br 5144  df-opab 5206  df-cnv 5693

This theorem is referenced by:  rnun  6165  funcnvpr  6628  funcnvtp  6629  funcnvqp  6630  f1oun  6867  f1oprswap  6892  suppun  8209  sbthlem8  9130  domss2  9176  cnvfi  9216  1sdomOLD  9285  fsuppun  9427  fpwwe2lem12  10682  trclublem  15034  mbfres2  25680  ex-cnv  30456  suppun2  32693  cnvprop  32705  padct  32731  cycpmconjslem2  33175  eulerpartlemt  34373  mthmpps  35587  clcnvlem  43636  frege131d  43777