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 ( ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 = 𝑦𝑥 𝑅 𝑦 ) ↔ ∀ 𝑥𝐴 𝑥 𝑅 𝑥 )