Theorem idinxpss

Description: Two ways to say that an intersection of the identity relation with a Cartesian product is a subclass. (Contributed by Peter Mazsa, 16-Jul-2019)

	Ref	Expression
Assertion	idinxpss	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		inxpss	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 I 𝑦 → 𝑥 𝑅 𝑦 ) )
2		ideqg	⊢ ( 𝑦 ∈ V → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
3	2	elv	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
4	3	imbi1i	⊢ ( ( 𝑥 I 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
5	4	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 I 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
6	1 5	bitri	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )