Step | Hyp | Ref | Expression |
1 |
|
bitr |
(x e. Dom (F |` A) <-> E. y x, y e. F |` A) -> (E. y x, y e. F |` A <-> x e. Dom F i^i A) -> (x e. Dom (F |` A) <-> x e. Dom F i^i A) |
2 |
|
eldm |
x e. Dom (F |` A) <-> E. y x, y e. F |` A |
3 |
1, 2 |
ax_mp |
(E. y x, y e. F |` A <-> x e. Dom F i^i A) -> (x e. Dom (F |` A) <-> x e. Dom F i^i A) |
4 |
|
bitr4 |
(E. y x, y e. F |` A <-> E. y (x, y e. F /\ x e. A)) -> (x e. Dom F i^i A <-> E. y (x, y e. F /\ x e. A)) -> (E. y x, y e. F |` A <-> x e. Dom F i^i A) |
5 |
|
prelres |
x, y e. F |` A <-> x, y e. F /\ x e. A |
6 |
5 |
exeqi |
E. y x, y e. F |` A <-> E. y (x, y e. F /\ x e. A) |
7 |
4, 6 |
ax_mp |
(x e. Dom F i^i A <-> E. y (x, y e. F /\ x e. A)) -> (E. y x, y e. F |` A <-> x e. Dom F i^i A) |
8 |
|
bitr |
(x e. Dom F i^i A <-> x e. Dom F /\ x e. A) -> (x e. Dom F /\ x e. A <-> E. y (x, y e. F /\ x e. A)) -> (x e. Dom F i^i A <-> E. y (x, y e. F /\ x e. A)) |
9 |
|
elin |
x e. Dom F i^i A <-> x e. Dom F /\ x e. A |
10 |
8, 9 |
ax_mp |
(x e. Dom F /\ x e. A <-> E. y (x, y e. F /\ x e. A)) -> (x e. Dom F i^i A <-> E. y (x, y e. F /\ x e. A)) |
11 |
|
bitr4 |
(x e. Dom F /\ x e. A <-> E. y x, y e. F /\ x e. A) ->
(E. y (x, y e. F /\ x e. A) <-> E. y x, y e. F /\ x e. A) ->
(x e. Dom F /\ x e. A <-> E. y (x, y e. F /\ x e. A)) |
12 |
|
eldm |
x e. Dom F <-> E. y x, y e. F |
13 |
12 |
aneq1i |
x e. Dom F /\ x e. A <-> E. y x, y e. F /\ x e. A |
14 |
11, 13 |
ax_mp |
(E. y (x, y e. F /\ x e. A) <-> E. y x, y e. F /\ x e. A) -> (x e. Dom F /\ x e. A <-> E. y (x, y e. F /\ x e. A)) |
15 |
|
exan2 |
E. y (x, y e. F /\ x e. A) <-> E. y x, y e. F /\ x e. A |
16 |
14, 15 |
ax_mp |
x e. Dom F /\ x e. A <-> E. y (x, y e. F /\ x e. A) |
17 |
10, 16 |
ax_mp |
x e. Dom F i^i A <-> E. y (x, y e. F /\ x e. A) |
18 |
7, 17 |
ax_mp |
E. y x, y e. F |` A <-> x e. Dom F i^i A |
19 |
3, 18 |
ax_mp |
x e. Dom (F |` A) <-> x e. Dom F i^i A |
20 |
19 |
eqri |
Dom (F |` A) == Dom F i^i A |