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 ⊢ A ⊆ V × W → A ⊆ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B

Proof

Step Hyp Ref Expression
1 ssel ⊢ A ⊆ B → x y ∈ A → x y ∈ B
2 1 alrimivv ⊢ A ⊆ B → ∀ x ∀ y x y ∈ A → x y ∈ B
3 ssel ⊢ A ⊆ V × W → z ∈ A → z ∈ V × W
4 elxpi ⊢ z ∈ V × W → ∃ x ∃ y z = x y ∧ x ∈ V ∧ y ∈ W
5 3 4 syl6 ⊢ A ⊆ V × W → z ∈ A → ∃ x ∃ y z = x y ∧ x ∈ V ∧ y ∈ W
6 eleq1 ⊢ z = x y → z ∈ A ↔ x y ∈ A
7 eleq1 ⊢ z = x y → z ∈ B ↔ x y ∈ B
8 6 7 imbi12d ⊢ z = x y → z ∈ A → z ∈ B ↔ x y ∈ A → x y ∈ B
9 8 adantr ⊢ z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B ↔ x y ∈ A → x y ∈ B
10 9 biimprcd ⊢ x y ∈ A → x y ∈ B → z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B
11 10 2alimi ⊢ ∀ x ∀ y x y ∈ A → x y ∈ B → ∀ x ∀ y z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B
12 19.23vv ⊢ ∀ x ∀ y z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B ↔ ∃ x ∃ y z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B
13 11 12 sylib ⊢ ∀ x ∀ y x y ∈ A → x y ∈ B → ∃ x ∃ y z = x y ∧ x ∈ V ∧ y ∈ W → z ∈ A → z ∈ B
14 5 13 sylan9 ⊢ A ⊆ V × W ∧ ∀ x ∀ y x y ∈ A → x y ∈ B → z ∈ A → z ∈ A → z ∈ B
15 14 pm2.43d ⊢ A ⊆ V × W ∧ ∀ x ∀ y x y ∈ A → x y ∈ B → z ∈ A → z ∈ B
16 15 ssrdv ⊢ A ⊆ V × W ∧ ∀ x ∀ y x y ∈ A → x y ∈ B → A ⊆ B
17 16 ex ⊢ A ⊆ V × W → ∀ x ∀ y x y ∈ A → x y ∈ B → A ⊆ B
18 2 17 impbid2 ⊢ A ⊆ V × W → A ⊆ B ↔ ∀ x ∀ y x y ∈ A → x y ∈ B