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

Metamath Proof Explorer

Theorem ercl

Description: Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses ersym.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
ersym.2 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion ercl ( 𝜑 → 𝐴 ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 ersym.1 ⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2 ersym.2 ⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3 errel ⊢ ( 𝑅 Er 𝑋 → Rel 𝑅 )
4 1 3 syl ⊢ ( 𝜑 → Rel 𝑅 )
5 releldm ⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )
6 4 2 5 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )
7 erdm ⊢ ( 𝑅 Er 𝑋 → dom 𝑅 = 𝑋 )
8 1 7 syl ⊢ ( 𝜑 → dom 𝑅 = 𝑋 )
9 6 8 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )