Step |
Hyp |
Ref |
Expression |
1 |
|
an4 |
|- ( ( ( x e. A /\ ph ) /\ ( x e. B /\ ps ) ) <-> ( ( x e. A /\ x e. B ) /\ ( ph /\ ps ) ) ) |
2 |
|
elin |
|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) ) |
3 |
2
|
anbi1i |
|- ( ( x e. ( A i^i B ) /\ ( ph /\ ps ) ) <-> ( ( x e. A /\ x e. B ) /\ ( ph /\ ps ) ) ) |
4 |
1 3
|
bitr4i |
|- ( ( ( x e. A /\ ph ) /\ ( x e. B /\ ps ) ) <-> ( x e. ( A i^i B ) /\ ( ph /\ ps ) ) ) |
5 |
4
|
abbii |
|- { x | ( ( x e. A /\ ph ) /\ ( x e. B /\ ps ) ) } = { x | ( x e. ( A i^i B ) /\ ( ph /\ ps ) ) } |
6 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
7 |
|
df-rab |
|- { x e. B | ps } = { x | ( x e. B /\ ps ) } |
8 |
6 7
|
ineq12i |
|- ( { x e. A | ph } i^i { x e. B | ps } ) = ( { x | ( x e. A /\ ph ) } i^i { x | ( x e. B /\ ps ) } ) |
9 |
|
inab |
|- ( { x | ( x e. A /\ ph ) } i^i { x | ( x e. B /\ ps ) } ) = { x | ( ( x e. A /\ ph ) /\ ( x e. B /\ ps ) ) } |
10 |
8 9
|
eqtri |
|- ( { x e. A | ph } i^i { x e. B | ps } ) = { x | ( ( x e. A /\ ph ) /\ ( x e. B /\ ps ) ) } |
11 |
|
df-rab |
|- { x e. ( A i^i B ) | ( ph /\ ps ) } = { x | ( x e. ( A i^i B ) /\ ( ph /\ ps ) ) } |
12 |
5 10 11
|
3eqtr4i |
|- ( { x e. A | ph } i^i { x e. B | ps } ) = { x e. ( A i^i B ) | ( ph /\ ps ) } |