Metamath Proof Explorer


Theorem idinxpssinxp

Description: Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 . (Contributed by Peter Mazsa, 6-Mar-2019)

Ref Expression
Assertion idinxpssinxp ( ( I ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥 = 𝑦𝑥 𝑅 𝑦 ) )

Proof

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