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

Theorem cnvco 5754
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 1869 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3412 . . . . 5 𝑥 ∈ V
3 vex 3412 . . . . 5 𝑦 ∈ V
42, 3brco 5739 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3412 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5751 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5751 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 630 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1855 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 306 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 5120 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5559 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5560 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2775 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1543  wex 1787   class class class wbr 5053  {copab 5115  ccnv 5550  ccom 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-cnv 5559  df-co 5560
This theorem is referenced by:  rncoss  5841  rncoeq  5844  dmco  6118  cores2  6123  co01  6125  coi2  6127  relcnvtrg  6130  dfdm2  6144  f1cof1  6626  f1coOLD  6628  cofunex2g  7723  fparlem3  7882  fparlem4  7883  suppco  7948  fsuppcolem  9017  relexpcnv  14598  relexpaddg  14616  cnvps  18084  gimco  18672  gsumzf1o  19297  cnco  22163  ptrescn  22536  qtopcn  22611  hmeoco  22669  cncombf  24555  deg1val  24994  fcoinver  30665  ofpreima  30722  cycpmconjv  31128  cycpmconjs  31142  cyc3conja  31143  mbfmco  31943  eulerpartlemmf  32054  cvmliftmolem1  32956  cvmlift2lem9a  32978  cvmlift2lem9  32986  mclsppslem  33258  ftc1anclem3  35589  trlcocnv  38471  tendoicl  38547  cdlemk45  38698  cononrel1  40878  cononrel2  40879  cnvtrcl0  40910  cnvtrrel  40955  relexpaddss  41003  frege131d  41049  brco2f1o  41319  brco3f1o  41320  clsneicnv  41392  neicvgnvo  41402  smfco  44008
  Copyright terms: Public domain W3C validator