Theorem idinxpssinxp3

Description: Identity intersection with a square Cartesian product in subclass relation with an intersection with the same Cartesian product. (Contributed by Peter Mazsa, 16-Mar-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	idinxpssinxp3	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ( I ↾ 𝐴 ) ⊆ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		idinxpssinxp2	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )
2		idrefALT	⊢ ( ( I ↾ 𝐴 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑥 )
3	1 2	bitr4i	⊢ ( ( I ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ↔ ( I ↾ 𝐴 ) ⊆ 𝑅 )