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

Metamath Proof Explorer

Theorem refrelcosslem

Description: Lemma for the left side of the refrelcoss3 reflexivity theorem. (Contributed by Peter Mazsa, 1-Apr-2019)

Ref Expression
Assertion refrelcosslem ⊢ ∀ x ∈ dom ⁡ ≀ R x ≀ R x

Proof

Step Hyp Ref Expression
1 ralel ⊢ ∀ x ∈ dom ⁡ ≀ R x ∈ dom ⁡ ≀ R
2 eldmcoss2 ⊢ x ∈ V → x ∈ dom ⁡ ≀ R ↔ x ≀ R x
3 2 elv ⊢ x ∈ dom ⁡ ≀ R ↔ x ≀ R x
4 3 ralbii ⊢ ∀ x ∈ dom ⁡ ≀ R x ∈ dom ⁡ ≀ R ↔ ∀ x ∈ dom ⁡ ≀ R x ≀ R x
5 1 4 mpbi ⊢ ∀ x ∈ dom ⁡ ≀ R x ≀ R x