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

Theorem cnvco 5896
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 1861 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3484 . . . . 5 𝑥 ∈ V
3 vex 3484 . . . . 5 𝑦 ∈ V
42, 3brco 5881 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3484 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5893 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5893 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 628 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1848 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 303 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 5210 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5693 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5694 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2775 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wex 1779   class class class wbr 5143  {copab 5205  ccnv 5684  ccom 5689
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  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-co 5694
This theorem is referenced by:  rncoss  5986  rncoeq  5990  dmco  6274  cores2  6279  co01  6281  coi2  6283  relcnvtrg  6286  dfdm2  6301  f1cof1  6814  cofunex2g  7974  fparlem3  8139  fparlem4  8140  suppco  8231  fsuppcolem  9441  relexpcnv  15074  relexpaddg  15092  cnvps  18623  gimco  19286  gsumzf1o  19930  cnco  23274  ptrescn  23647  qtopcn  23722  hmeoco  23780  cncombf  25693  deg1val  26135  fcoinver  32617  ofpreima  32675  cycpmconjv  33162  cycpmconjs  33176  cyc3conja  33177  mbfmco  34266  eulerpartlemmf  34377  cvmliftmolem1  35286  cvmlift2lem9a  35308  cvmlift2lem9  35316  mclsppslem  35588  ftc1anclem3  37702  trlcocnv  40722  tendoicl  40798  cdlemk45  40949  rimco  42528  cononrel1  43607  cononrel2  43608  cnvtrcl0  43639  cnvtrrel  43683  relexpaddss  43731  frege131d  43777  brco2f1o  44045  brco3f1o  44046  clsneicnv  44118  neicvgnvo  44128  smfco  46817
  Copyright terms: Public domain W3C validator