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 𝐴 → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relcnv Rel 𝐴
2 elrelimasn ( Rel 𝐴 → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 ) )
3 1 2 ax-mp ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐵 𝐴 𝐶 )
4 relbrcnvg ( Rel 𝐴 → ( 𝐵 𝐴 𝐶𝐶 𝐴 𝐵 ) )
5 3 4 syl5bb ( Rel 𝐴 → ( 𝐶 ∈ ( 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) )