MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelcnv Unicode version

Theorem opelcnv 5138
Description: Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
Hypotheses
Ref Expression
opelcnv.1
opelcnv.2
Assertion
Ref Expression
opelcnv

Proof of Theorem opelcnv
StepHypRef Expression
1 opelcnv.1 . 2
2 opelcnv.2 . 2
3 opelcnvg 5136 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1758   cvv 3081  <.cop 3999  `'ccnv 4956
This theorem is referenced by:  cnvopab  5357  cnv0  5359  cnvdif  5362  dfrel2  5407  cnvcnvsn  5435  cnvresima  5446  dfco2  5456  cnviin  5493  fcnvres  5710  cnvf1olem  6804  cnvimadfsn  6833  dmtpos  6891  dftpos4  6898  tpostpos  6899  brsdom2  7569  fsumcom2  13399  gsumcom2  16636  metustsymOLD  20535  metustsym  20536  fprodcom2  27951  cnvco1  28026  cnvco2  28027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-br 4410  df-opab 4468  df-cnv 4965
  Copyright terms: Public domain W3C validator