Metamath Proof Explorer

Theorem bj-ssrel

Description: Variant of ssrel where the antecedent is more versatile than Rel A (the proof is shorter than that of ssrel , which can be proved from this one using sylbi and df-rel , and of ssrel2 , which uses restricted quantifiers). (Contributed by BJ, 7-Nov-2026)

Ref Expression
Assertion bj-ssrel ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
2 1 alrimivv ⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
3 ssel ⊢ ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( 𝑉 × 𝑊 ) ) )
4 elxpi ⊢ ( 𝑧 ∈ ( 𝑉 × 𝑊 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) )
5 3 4 syl6 ⊢ ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) → ( 𝑧 ∈ 𝐴 → ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) ) )
6 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐴 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 ) )
7 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ 𝐵 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) )
8 6 7 imbi12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
9 8 adantr ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )
10 9 biimprcd ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
11 10 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
12 19.23vv ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
13 11 12 sylib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑊 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
14 5 13 sylan9 ⊢ ( ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) ) )
15 14 pm2.43d ⊢ ( ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝐵 ) )
16 15 ssrdv ⊢ ( ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) ∧ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) → 𝐴 ⊆ 𝐵 )
17 16 ex ⊢ ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) → ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) → 𝐴 ⊆ 𝐵 ) )
18 2 17 impbid2 ⊢ ( 𝐴 ⊆ ( 𝑉 × 𝑊 ) → ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐵 ) ) )