![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opelcnv | Structured version Visualization version GIF version |
Description: Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995.) |
Ref | Expression |
---|---|
opelcnv.1 | ⊢ 𝐴 ∈ V |
opelcnv.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
opelcnv | ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelcnv.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | opelcnv.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | opelcnvg 5878 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅)) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ (〈𝐴, 𝐵〉 ∈ ◡𝑅 ↔ 〈𝐵, 𝐴〉 ∈ 𝑅) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∈ wcel 2106 Vcvv 3474 〈cop 4633 ◡ccnv 5674 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-br 5148 df-opab 5210 df-cnv 5683 |
This theorem is referenced by: cnvopab 6135 cnvdif 6140 dfrel2 6185 cnvcnvsn 6215 cnvresima 6226 dfco2 6241 cnviin 6282 fcnvres 6765 cnvf1olem 8092 cnvimadfsn 8153 dmtpos 8219 dftpos4 8226 tpostpos 8227 brsdom2 9093 fsumcom2 15716 fprodcom2 15924 gsumcom2 19837 metustsym 24055 gsumhashmul 32195 cnvco1 34717 cnvco2 34718 cnviun 42386 |
Copyright terms: Public domain | W3C validator |