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

Theorem cnvco 5749
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 1852 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3495 . . . . 5 𝑥 ∈ V
3 vex 3495 . . . . 5 𝑦 ∈ V
42, 3brco 5734 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3495 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5746 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5746 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 626 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1839 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 304 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 5124 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5556 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5557 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2851 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wex 1771   class class class wbr 5057  {copab 5119  ccnv 5547  ccom 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-cnv 5556  df-co 5557
This theorem is referenced by:  rncoss  5836  rncoeq  5839  dmco  6100  cores2  6105  co01  6107  coi2  6109  relcnvtrg  6112  dfdm2  6125  f1co  6578  cofunex2g  7640  fparlem3  7798  fparlem4  7799  suppco  7859  supp0cosupp0OLD  7862  imacosuppOLD  7864  fsuppcolem  8852  relexpcnv  14382  relexpaddg  14400  cnvps  17810  gimco  18346  gsumzf1o  18961  cnco  21802  ptrescn  22175  qtopcn  22250  hmeoco  22308  cncombf  24186  deg1val  24617  fcoinver  30285  ofpreima  30338  cycpmconjv  30711  cycpmconjs  30725  cyc3conja  30726  mbfmco  31421  eulerpartlemmf  31532  cvmliftmolem1  32425  cvmlift2lem9a  32447  cvmlift2lem9  32455  mclsppslem  32727  ftc1anclem3  34850  trlcocnv  37736  tendoicl  37812  cdlemk45  37963  cononrel1  39832  cononrel2  39833  cnvtrcl0  39864  cnvtrrel  39893  relexpaddss  39941  frege131d  39987  brco2f1o  40260  brco3f1o  40261  clsneicnv  40333  neicvgnvo  40343  smfco  42954
  Copyright terms: Public domain W3C validator