Theorem opelcnv 5122

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

Step	Hyp	Ref	Expression
1		opelcnv.1	. 2 |- A e. _V
2		opelcnv.2	. 2 |- B e. _V
3		opelcnvg 5120	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( <. A , B >. e. `' R <-> <. B , A >. e. R ) )
4	1, 2, 3	mp2an 672	1 |- ( <. A , B >. e. `' R <-> <. B , A >. e. R )

Syntax hints:   <-> wb 184   e. wcel 1758   _Vcvv 3071   <.cop 3984   `'ccnv 4940

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 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632

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 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-br 4394  df-opab 4452  df-cnv 4949

This theorem is referenced by:  cnvopab  5339  cnv0  5341  cnvdif  5344  dfrel2  5389  cnvcnvsn  5417  cnvresima  5428  dfco2  5438  cnviin  5475  fcnvres  5689  cnvf1olem  6773  cnvimadfsn  6802  dmtpos  6860  dftpos4  6867  tpostpos  6868  brsdom2  7538  fsumcom2  13352  gsumcom2  16581  metustsymOLD  20261  metustsym  20262  fprodcom2  27632  cnvco1  27707  cnvco2  27708