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

Theorem cnvco 5340
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 1827 . . . 4 (∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
2 vex 3234 . . . . 5 𝑥 ∈ V
3 vex 3234 . . . . 5 𝑦 ∈ V
42, 3brco 5325 . . . 4 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧𝑧𝐴𝑦))
5 vex 3234 . . . . . . 7 𝑧 ∈ V
63, 5brcnv 5337 . . . . . 6 (𝑦𝐴𝑧𝑧𝐴𝑦)
75, 2brcnv 5337 . . . . . 6 (𝑧𝐵𝑥𝑥𝐵𝑧)
86, 7anbi12i 733 . . . . 5 ((𝑦𝐴𝑧𝑧𝐵𝑥) ↔ (𝑧𝐴𝑦𝑥𝐵𝑧))
98exbii 1814 . . . 4 (∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦𝑥𝐵𝑧))
101, 4, 93bitr4i 292 . . 3 (𝑥(𝐴𝐵)𝑦 ↔ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥))
1110opabbii 4750 . 2 {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
12 df-cnv 5151 . 2 (𝐴𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴𝐵)𝑦}
13 df-co 5152 . 2 (𝐵𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦𝐴𝑧𝑧𝐵𝑥)}
1411, 12, 133eqtr4i 2683 1 (𝐴𝐵) = (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wex 1744   class class class wbr 4685  {copab 4745  ccnv 5142  ccom 5147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-cnv 5151  df-co 5152
This theorem is referenced by:  rncoss  5418  rncoeq  5421  dmco  5681  cores2  5686  co01  5688  coi2  5690  relcnvtr  5693  dfdm2  5705  f1co  6148  cofunex2g  7173  fparlem3  7324  fparlem4  7325  supp0cosupp0  7379  imacosupp  7380  fsuppcolem  8347  relexpcnv  13819  relexpaddg  13837  cnvps  17259  gimco  17757  gsumzf1o  18359  cnco  21118  ptrescn  21490  qtopcn  21565  hmeoco  21623  cncombf  23470  deg1val  23901  fcoinver  29544  ofpreima  29593  mbfmco  30454  eulerpartlemmf  30565  cvmliftmolem1  31389  cvmlift2lem9a  31411  cvmlift2lem9  31419  mclsppslem  31606  ftc1anclem3  33617  trlcocnv  36325  tendoicl  36401  cdlemk45  36552  cononrel1  38217  cononrel2  38218  cnvtrcl0  38250  cnvtrrel  38279  relexpaddss  38327  frege131d  38373  brco2f1o  38647  brco3f1o  38648  clsneicnv  38720  neicvgnvo  38730  smfco  41330
  Copyright terms: Public domain W3C validator