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

Metamath Proof Explorer

Theorem eliniseg2

Description: Eliminate the class existence constraint in eliniseg . (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 17-Nov-2015)

Ref Expression
Assertion eliniseg2 ⊢ Rel ⁡ A → C ∈ A -1 B ↔ C A B

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ A -1
2 elrelimasn ⊢ Rel ⁡ A -1 → C ∈ A -1 B ↔ B A -1 C
3 1 2 ax-mp ⊢ C ∈ A -1 B ↔ B A -1 C
4 relbrcnvg ⊢ Rel ⁡ A → B A -1 C ↔ C A B
5 3 4 bitrid ⊢ Rel ⁡ A → C ∈ A -1 B ↔ C A B