Theorem opelcnv 5866

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

Step	Hyp	Ref	Expression
1		opelcnv.1	. 2 ⊢ 𝐴 ∈ V
2		opelcnv.2	. 2 ⊢ 𝐵 ∈ V
3		opelcnvg 5865	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅))
4	1, 2, 3	mp2an 692	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ ◡𝑅 ↔ ⟨𝐵, 𝐴⟩ ∈ 𝑅)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  Vcvv 3464  ⟨cop 4612  ^◡ccnv 5658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-cnv 5667

This theorem is referenced by:  cnvopab  6131  cnvopabOLD  6132  cnvdif  6137  dfrel2  6183  cnvcnvsn  6213  cnvresima  6224  dfco2  6239  cnviin  6280  fcnvres  6760  cnvf1olem  8114  cnvimadfsn  8176  dmtpos  8242  dftpos4  8249  tpostpos  8250  brsdom2  9116  fsumcom2  15795  fprodcom2  16005  gsumcom2  19961  metustsym  24499  gsumhashmul  33060  cnvco1  35781  cnvco2  35782  cnviun  43641  tposideq  48830