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

Theorem cnvco 5898
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 1858 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3481 . . . . 5 𝑥 ∈ V
3 vex 3481 . . . . 5 𝑦 ∈ V
42, 3brco 5883 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3481 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5895 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5895 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 628 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1844 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 303 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 5214 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5696 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5697 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2772 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1536  wex 1775   class class class wbr 5147  {copab 5209  ccnv 5687  ccom 5692
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  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-cnv 5696  df-co 5697
This theorem is referenced by:  rncoss  5988  rncoeq  5992  dmco  6275  cores2  6280  co01  6282  coi2  6284  relcnvtrg  6287  dfdm2  6302  f1cof1  6814  cofunex2g  7972  fparlem3  8137  fparlem4  8138  suppco  8229  fsuppcolem  9438  relexpcnv  15070  relexpaddg  15088  cnvps  18635  gimco  19298  gsumzf1o  19944  cnco  23289  ptrescn  23662  qtopcn  23737  hmeoco  23795  cncombf  25706  deg1val  26149  fcoinver  32623  ofpreima  32681  cycpmconjv  33144  cycpmconjs  33158  cyc3conja  33159  mbfmco  34245  eulerpartlemmf  34356  cvmliftmolem1  35265  cvmlift2lem9a  35287  cvmlift2lem9  35295  mclsppslem  35567  ftc1anclem3  37681  trlcocnv  40702  tendoicl  40778  cdlemk45  40929  rimco  42504  cononrel1  43583  cononrel2  43584  cnvtrcl0  43615  cnvtrrel  43659  relexpaddss  43707  frege131d  43753  brco2f1o  44021  brco3f1o  44022  clsneicnv  44094  neicvgnvo  44104  smfco  46757
  Copyright terms: Public domain W3C validator