Step |
Hyp |
Ref |
Expression |
1 |
|
xrnss3v |
|- ( R |X. S ) C_ ( _V X. ( _V X. _V ) ) |
2 |
1
|
brel |
|- ( A ( R |X. S ) B -> ( A e. _V /\ B e. ( _V X. _V ) ) ) |
3 |
2
|
simprd |
|- ( A ( R |X. S ) B -> B e. ( _V X. _V ) ) |
4 |
|
elvv |
|- ( B e. ( _V X. _V ) <-> E. x E. y B = <. x , y >. ) |
5 |
3 4
|
sylib |
|- ( A ( R |X. S ) B -> E. x E. y B = <. x , y >. ) |
6 |
5
|
pm4.71ri |
|- ( A ( R |X. S ) B <-> ( E. x E. y B = <. x , y >. /\ A ( R |X. S ) B ) ) |
7 |
|
19.41vv |
|- ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> ( E. x E. y B = <. x , y >. /\ A ( R |X. S ) B ) ) |
8 |
|
breq2 |
|- ( B = <. x , y >. -> ( A ( R |X. S ) B <-> A ( R |X. S ) <. x , y >. ) ) |
9 |
8
|
pm5.32i |
|- ( ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) ) |
10 |
9
|
2exbii |
|- ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) B ) <-> E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) ) |
11 |
6 7 10
|
3bitr2i |
|- ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) ) |
12 |
|
brxrn |
|- ( ( A e. V /\ x e. _V /\ y e. _V ) -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) ) |
13 |
12
|
el3v23 |
|- ( A e. V -> ( A ( R |X. S ) <. x , y >. <-> ( A R x /\ A S y ) ) ) |
14 |
13
|
anbi2d |
|- ( A e. V -> ( ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) ) ) |
15 |
|
3anass |
|- ( ( B = <. x , y >. /\ A R x /\ A S y ) <-> ( B = <. x , y >. /\ ( A R x /\ A S y ) ) ) |
16 |
14 15
|
bitr4di |
|- ( A e. V -> ( ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> ( B = <. x , y >. /\ A R x /\ A S y ) ) ) |
17 |
16
|
2exbidv |
|- ( A e. V -> ( E. x E. y ( B = <. x , y >. /\ A ( R |X. S ) <. x , y >. ) <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) ) |
18 |
11 17
|
syl5bb |
|- ( A e. V -> ( A ( R |X. S ) B <-> E. x E. y ( B = <. x , y >. /\ A R x /\ A S y ) ) ) |