MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvco Structured version   Visualization version   GIF version

Theorem cnvco 5503
Description: Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
cnvco (𝐴𝐵) = (𝐵𝐴)

Proof of Theorem cnvco
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 exancom 1947 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3390 . . . . 5 𝑥 ∈ V
3 vex 3390 . . . . 5 𝑦 ∈ V
42, 3brco 5488 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3390 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5500 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5500 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 614 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1933 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 294 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 4904 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5313 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5314 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2834 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wex 1859   class class class wbr 4837  {copab 4899  ccnv 5304  ccom 5309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-sep 4968  ax-nul 4977  ax-pr 5090
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-br 4838  df-opab 4900  df-cnv 5313  df-co 5314
This theorem is referenced by:  rncoss  5581  rncoeq  5584  dmco  5851  cores2  5856  co01  5858  coi2  5860  relcnvtr  5863  dfdm2  5875  f1co  6320  cofunex2g  7355  fparlem3  7507  fparlem4  7508  supp0cosupp0  7563  imacosupp  7564  fsuppcolem  8539  relexpcnv  13992  relexpaddg  14010  cnvps  17411  gimco  17906  gsumzf1o  18508  cnco  21278  ptrescn  21650  qtopcn  21725  hmeoco  21783  cncombf  23633  deg1val  24064  fcoinver  29737  ofpreima  29786  mbfmco  30645  eulerpartlemmf  30756  cvmliftmolem1  31580  cvmlift2lem9a  31602  cvmlift2lem9  31610  mclsppslem  31797  ftc1anclem3  33793  trlcocnv  36495  tendoicl  36571  cdlemk45  36722  cononrel1  38394  cononrel2  38395  cnvtrcl0  38427  cnvtrrel  38456  relexpaddss  38504  frege131d  38550  brco2f1o  38824  brco3f1o  38825  clsneicnv  38897  neicvgnvo  38907  smfco  41485
  Copyright terms: Public domain W3C validator