This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem opelcnv

Description: Ordered-pair membership in converse relation. (Contributed by NM, 13-Aug-1995)

Ref Expression
Hypotheses opelcnv.1 ⊢ A ∈ V
opelcnv.2 ⊢ B ∈ V
Assertion opelcnv ⊢ A B ∈ R -1 ↔ B A ∈ R

Proof

Step Hyp Ref Expression
1 opelcnv.1 ⊢ A ∈ V
2 opelcnv.2 ⊢ B ∈ V
3 opelcnvg ⊢ A ∈ V ∧ B ∈ V → A B ∈ R -1 ↔ B A ∈ R
4 1 2 3 mp2an ⊢ A B ∈ R -1 ↔ B A ∈ R