Step |
Hyp |
Ref |
Expression |
1 |
|
3anass |
|- ( ( w = <. x , y >. /\ u R x /\ u S y ) <-> ( w = <. x , y >. /\ ( u R x /\ u S y ) ) ) |
2 |
1
|
3exbii |
|- ( E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) <-> E. u E. x E. y ( w = <. x , y >. /\ ( u R x /\ u S y ) ) ) |
3 |
|
exrot3 |
|- ( E. u E. x E. y ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> E. x E. y E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) ) |
4 |
|
19.42v |
|- ( E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) ) |
5 |
4
|
2exbii |
|- ( E. x E. y E. u ( w = <. x , y >. /\ ( u R x /\ u S y ) ) <-> E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) ) |
6 |
2 3 5
|
3bitri |
|- ( E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) <-> E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) ) |
7 |
6
|
abbii |
|- { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) } = { w | E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) } |
8 |
|
dfrn6 |
|- ran ( R |X. S ) = { w | [ w ] `' ( R |X. S ) =/= (/) } |
9 |
|
n0 |
|- ( [ w ] `' ( R |X. S ) =/= (/) <-> E. u u e. [ w ] `' ( R |X. S ) ) |
10 |
|
elec1cnvxrn2 |
|- ( u e. _V -> ( u e. [ w ] `' ( R |X. S ) <-> E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) ) ) |
11 |
10
|
elv |
|- ( u e. [ w ] `' ( R |X. S ) <-> E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) ) |
12 |
11
|
exbii |
|- ( E. u u e. [ w ] `' ( R |X. S ) <-> E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) ) |
13 |
9 12
|
bitri |
|- ( [ w ] `' ( R |X. S ) =/= (/) <-> E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) ) |
14 |
13
|
abbii |
|- { w | [ w ] `' ( R |X. S ) =/= (/) } = { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) } |
15 |
8 14
|
eqtri |
|- ran ( R |X. S ) = { w | E. u E. x E. y ( w = <. x , y >. /\ u R x /\ u S y ) } |
16 |
|
df-opab |
|- { <. x , y >. | E. u ( u R x /\ u S y ) } = { w | E. x E. y ( w = <. x , y >. /\ E. u ( u R x /\ u S y ) ) } |
17 |
7 15 16
|
3eqtr4i |
|- ran ( R |X. S ) = { <. x , y >. | E. u ( u R x /\ u S y ) } |