Step | Hyp | Ref | Expression |
1 |
|
ex2ssg |
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) -> l1, l2 e. ex2 R -> l1, l2 e. ex2 S |
2 |
|
bi1 |
(x, y e. R <-> x, y e. S) -> x, y e. R -> x, y e. S |
3 |
2 |
imim2i |
(x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S |
4 |
3 |
alimi |
A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) |
5 |
4 |
alimi |
A. x A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> A. x A. y (x IN l1 /\ y IN l2 -> x, y e. R -> x, y e. S) |
6 |
1, 5 |
syl |
A. x A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> l1, l2 e. ex2 R -> l1, l2 e. ex2 S |
7 |
|
ex2ssg |
A. x A. y (x IN l1 /\ y IN l2 -> x, y e. S -> x, y e. R) -> l1, l2 e. ex2 S -> l1, l2 e. ex2 R |
8 |
|
bi2 |
(x, y e. R <-> x, y e. S) -> x, y e. S -> x, y e. R |
9 |
8 |
imim2i |
(x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> x IN l1 /\ y IN l2 -> x, y e. S -> x, y e. R |
10 |
9 |
alimi |
A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> A. y (x IN l1 /\ y IN l2 -> x, y e. S -> x, y e. R) |
11 |
10 |
alimi |
A. x A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> A. x A. y (x IN l1 /\ y IN l2 -> x, y e. S -> x, y e. R) |
12 |
7, 11 |
syl |
A. x A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> l1, l2 e. ex2 S -> l1, l2 e. ex2 R |
13 |
6, 12 |
ibid |
A. x A. y (x IN l1 /\ y IN l2 -> (x, y e. R <-> x, y e. S)) -> (l1, l2 e. ex2 R <-> l1, l2 e. ex2 S) |