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

Theorem opelcnv 5015
Description: Ordered-pair membership in converse. (Contributed by NM, 13-Aug-1995.)
Hypotheses
Ref Expression
opelcnv.1  |-  A  e. 
_V
opelcnv.2  |-  B  e. 
_V
Assertion
Ref Expression
opelcnv  |-  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R )

Proof of Theorem opelcnv
StepHypRef Expression
1 opelcnv.1 . 2  |-  A  e. 
_V
2 opelcnv.2 . 2  |-  B  e. 
_V
3 opelcnvg 5013 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R ) )
41, 2, 3mp2an 677 1  |-  ( <. A ,  B >.  e.  `' R  <->  <. B ,  A >.  e.  R )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1886   _Vcvv 3044   <.cop 3973   `'ccnv 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-cnv 4841
This theorem is referenced by:  cnvopab  5236  cnv0  5238  cnvdif  5241  dfrel2  5285  cnvcnvsn  5312  cnvresima  5323  dfco2  5333  cnviin  5372  fcnvres  5758  cnvf1olem  6891  cnvimadfsn  6920  dmtpos  6982  dftpos4  6989  tpostpos  6990  brsdom2  7693  fsumcom2  13828  fprodcom2  14031  gsumcom2  17600  metustsym  21563  cnvco1  30393  cnvco2  30394  cnviun  36236
  Copyright terms: Public domain W3C validator