Step |
Hyp |
Ref |
Expression |
1 |
|
an4 |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) |
2 |
|
elin |
⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) |
3 |
2
|
anbi1i |
⊢ ( ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) |
4 |
1 3
|
bitr4i |
⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) ↔ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) |
5 |
4
|
abbii |
⊢ { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) } = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) } |
6 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
7 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐵 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) } |
8 |
6 7
|
ineq12i |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) } ) |
9 |
|
inab |
⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∩ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) } ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) } |
10 |
8 9
|
eqtri |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ) } |
11 |
|
df-rab |
⊢ { 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∣ ( 𝜑 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝜑 ∧ 𝜓 ) ) } |
12 |
5 10 11
|
3eqtr4i |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) = { 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ∣ ( 𝜑 ∧ 𝜓 ) } |