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

Metamath Proof Explorer

Theorem ref5

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

		Ref	Expression
	Assertion	ref5	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
2	1	imbi1i	⊢ ( ( 𝑦 = 𝑥 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
3	2	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 = 𝑥 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
4		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑥 ) )
5	4	ceqsralbv	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 = 𝑥 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
6	3 5	bitr3i	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
7	6	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
8		idinxpss	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
9		ralin	⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
10	7 8 9	3bitr4i	⊢ ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) 𝑥 𝑅 𝑥 )