Theorem cnvref5

Description: Two ways to say that a relation is a subclass of the identity relation. (Contributed by Peter Mazsa, 26-Jun-2019)

	Ref	Expression
Assertion	cnvref5	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssrel3	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ) )
2		ideqg	⊢ ( 𝑦 ∈ V → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
3	2	elv	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
4	3	imbi2i	⊢ ( ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) )
5	4	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) )
6	1 5	bitrdi	⊢ ( Rel 𝑅 → ( 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) )