Description: Two ways to say that intersections with Cartesian products are in a subclass relation, special case of inxpss2 . (Contributed by Peter Mazsa, 4-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | inxpssidinxp | ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inxpss2 | ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ) | |
2 | ideqg | ⊢ ( 𝑦 ∈ V → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) ) | |
3 | 2 | elv | ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) |
4 | 3 | imbi2i | ⊢ ( ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ↔ ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) |
5 | 4 | 2ralbii | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → 𝑥 I 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) |
6 | 1 5 | bitri | ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( I ∩ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝑥 𝑅 𝑦 → 𝑥 = 𝑦 ) ) |