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

Theorem opelcnv 5830
Description: Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.)
Hypotheses
Ref Expression
opelcnv.1 𝐴 ∈ V
opelcnv.2 𝐵 ∈ V
Assertion
Ref Expression
opelcnv (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)

Proof of Theorem opelcnv
StepHypRef Expression
1 opelcnv.1 . 2 𝐴 ∈ V
2 opelcnv.2 . 2 𝐵 ∈ V
3 opelcnvg 5829 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
41, 2, 3mp2an 693 1 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wcel 2114  Vcvv 3430  cop 4574  ccnv 5623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-cnv 5632
This theorem is referenced by:  cnvopab  6094  cnvopabOLD  6095  cnvdif  6101  dfrel2  6147  cnvcnvsn  6177  cnvresima  6188  dfco2  6203  cnviin  6244  fcnvres  6711  cnvf1olem  8053  cnvimadfsn  8115  dmtpos  8181  dftpos4  8188  tpostpos  8189  brsdom2  9032  fsumcom2  15727  fprodcom2  15940  gsumcom2  19941  metustsym  24530  gsumhashmul  33143  cnvco1  35957  cnvco2  35958  cnviun  44095  tposideq  49375
  Copyright terms: Public domain W3C validator