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 ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )

Proof

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