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

Metamath Proof Explorer

Theorem idrefALT

Description: Alternate proof of idref not relying on definitions related to functions. Two ways to state that a relation is reflexive on a class. (Contributed by FL, 15-Jan-2012) (Proof shortened by Mario Carneiro, 3-Nov-2015) (Revised by NM, 30-Mar-2016) (Proof shortened by BJ, 28-Aug-2022) The "proof modification is discouraged" tag is here only because this is an *ALT result. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion idrefALT ⊢ I ↾ A ⊆ R ↔ ∀ x ∈ A x R x

Proof

Step Hyp Ref Expression
1 df-ss ⊢ I ↾ A ⊆ R ↔ ∀ y y ∈ I ↾ A → y ∈ R
2 elrid ⊢ y ∈ I ↾ A ↔ ∃ x ∈ A y = x x
3 2 imbi1i ⊢ y ∈ I ↾ A → y ∈ R ↔ ∃ x ∈ A y = x x → y ∈ R
4 r19.23v ⊢ ∀ x ∈ A y = x x → y ∈ R ↔ ∃ x ∈ A y = x x → y ∈ R
5 eleq1 ⊢ y = x x → y ∈ R ↔ x x ∈ R
6 df-br ⊢ x R x ↔ x x ∈ R
7 5 6 bitr4di ⊢ y = x x → y ∈ R ↔ x R x
8 7 pm5.74i ⊢ y = x x → y ∈ R ↔ y = x x → x R x
9 8 ralbii ⊢ ∀ x ∈ A y = x x → y ∈ R ↔ ∀ x ∈ A y = x x → x R x
10 3 4 9 3bitr2i ⊢ y ∈ I ↾ A → y ∈ R ↔ ∀ x ∈ A y = x x → x R x
11 10 albii ⊢ ∀ y y ∈ I ↾ A → y ∈ R ↔ ∀ y ∀ x ∈ A y = x x → x R x
12 ralcom4 ⊢ ∀ x ∈ A ∀ y y = x x → x R x ↔ ∀ y ∀ x ∈ A y = x x → x R x
13 opex ⊢ x x ∈ V
14 biidd ⊢ y = x x → x R x ↔ x R x
15 13 14 ceqsalv ⊢ ∀ y y = x x → x R x ↔ x R x
16 15 ralbii ⊢ ∀ x ∈ A ∀ y y = x x → x R x ↔ ∀ x ∈ A x R x
17 11 12 16 3bitr2i ⊢ ∀ y y ∈ I ↾ A → y ∈ R ↔ ∀ x ∈ A x R x
18 1 17 bitri ⊢ I ↾ A ⊆ R ↔ ∀ x ∈ A x R x