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 𝐴 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | ⊢ Rel ◡ 𝐴 | |
2 | elrelimasn | ⊢ ( Rel ◡ 𝐴 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐵 ◡ 𝐴 𝐶 ) ) | |
3 | 1 2 | ax-mp | ⊢ ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐵 ◡ 𝐴 𝐶 ) |
4 | relbrcnvg | ⊢ ( Rel 𝐴 → ( 𝐵 ◡ 𝐴 𝐶 ↔ 𝐶 𝐴 𝐵 ) ) | |
5 | 3 4 | syl5bb | ⊢ ( Rel 𝐴 → ( 𝐶 ∈ ( ◡ 𝐴 “ { 𝐵 } ) ↔ 𝐶 𝐴 𝐵 ) ) |