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

Metamath Proof Explorer

Theorem idinxpssinxp4

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product (see also idinxpssinxp2 ). (Contributed by Peter Mazsa, 8-Mar-2019)

		Ref	Expression
	Assertion	idinxpssinxp4	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		idinxpssinxp	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) )
2		idinxpssinxp2	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )
3	1 2	bitr3i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )