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 C_ ( V X. W ) -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( <. x , y >. e. A -> <. x , y >. e. B ) )
2 1 alrimivv 
 |-  ( A C_ B -> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) )
3 ssel 
 |-  ( A C_ ( V X. W ) -> ( z e. A -> z e. ( V X. W ) ) )
4 elxpi 
 |-  ( z e. ( V X. W ) -> E. x E. y ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) )
5 3 4 syl6 
 |-  ( A C_ ( V X. W ) -> ( z e. A -> E. x E. y ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) ) )
6 eleq1 
 |-  ( z = <. x , y >. -> ( z e. A <-> <. x , y >. e. A ) )
7 eleq1 
 |-  ( z = <. x , y >. -> ( z e. B <-> <. x , y >. e. B ) )
8 6 7 imbi12d 
 |-  ( z = <. x , y >. -> ( ( z e. A -> z e. B ) <-> ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
9 8 adantr 
 |-  ( ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( ( z e. A -> z e. B ) <-> ( <. x , y >. e. A -> <. x , y >. e. B ) ) )
10 9 biimprcd 
 |-  ( ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( z e. A -> z e. B ) ) )
11 10 2alimi 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> A. x A. y ( ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( z e. A -> z e. B ) ) )
12 19.23vv 
 |-  ( A. x A. y ( ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( z e. A -> z e. B ) ) <-> ( E. x E. y ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( z e. A -> z e. B ) ) )
13 11 12 sylib 
 |-  ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> ( E. x E. y ( z = <. x , y >. /\ ( x e. V /\ y e. W ) ) -> ( z e. A -> z e. B ) ) )
14 5 13 sylan9 
 |-  ( ( A C_ ( V X. W ) /\ A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) -> ( z e. A -> ( z e. A -> z e. B ) ) )
15 14 pm2.43d 
 |-  ( ( A C_ ( V X. W ) /\ A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) -> ( z e. A -> z e. B ) )
16 15 ssrdv 
 |-  ( ( A C_ ( V X. W ) /\ A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) -> A C_ B )
17 16 ex 
 |-  ( A C_ ( V X. W ) -> ( A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) -> A C_ B ) )
18 2 17 impbid2 
 |-  ( A C_ ( V X. W ) -> ( A C_ B <-> A. x A. y ( <. x , y >. e. A -> <. x , y >. e. B ) ) )