Theorem cnvun 6149

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 5686	. . 3 ⊢ ◡(𝐴 ∪ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
2		unopab 5231	. . . 4 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
3		brun 5200	. . . . 5 ⊢ (𝑦(𝐴 ∪ 𝐵)𝑥 ↔ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥))
4	3	opabbii 5216	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥} = {⟨𝑥, 𝑦⟩ ∣ (𝑦𝐴𝑥 ∨ 𝑦𝐵𝑥)}
5	2, 4	eqtr4i 2756	. . 3 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}) = {⟨𝑥, 𝑦⟩ ∣ 𝑦(𝐴 ∪ 𝐵)𝑥}
6	1, 5	eqtr4i 2756	. 2 ⊢ ◡(𝐴 ∪ 𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
7		df-cnv 5686	. . 3 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
8		df-cnv 5686	. . 3 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
9	7, 8	uneq12i 4158	. 2 ⊢ (◡𝐴 ∪ ◡𝐵) = ({⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ∪ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
10	6, 9	eqtr4i 2756	1 ⊢ ◡(𝐴 ∪ 𝐵) = (◡𝐴 ∪ ◡𝐵)

Syntax hints:   ∨ wo 845   = wceq 1533   ∪ cun 3942   class class class wbr 5149  {copab 5211  ^◡ccnv 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-un 3949  df-br 5150  df-opab 5212  df-cnv 5686

This theorem is referenced by:  rnun  6152  funcnvpr  6616  funcnvtp  6617  funcnvqp  6618  f1oun  6857  f1oprswap  6882  suppun  8189  sbthlem8  9115  domss2  9161  cnvfi  9205  1sdomOLD  9274  fsuppun  9412  fpwwe2lem12  10667  trclublem  14978  mbfres2  25618  ex-cnv  30319  cnvprop  32558  padct  32583  cycpmconjslem2  32968  eulerpartlemt  34122  mthmpps  35323  clcnvlem  43195  frege131d  43336