Metamath Proof Explorer

Theorem inab

Description: Intersection of two class abstractions. (Contributed by NM, 29-Sep-2002) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion inab ⊢ x | φ ∩ x | ψ = x | φ ∧ ψ

Proof

Step Hyp Ref Expression
1 sban ⊢ y x φ ∧ ψ ↔ y x φ ∧ y x ψ
2 df-clab ⊢ y ∈ x | φ ∧ ψ ↔ y x φ ∧ ψ
3 df-clab ⊢ y ∈ x | φ ↔ y x φ
4 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
5 3 4 anbi12i ⊢ y ∈ x | φ ∧ y ∈ x | ψ ↔ y x φ ∧ y x ψ
6 1 2 5 3bitr4ri ⊢ y ∈ x | φ ∧ y ∈ x | ψ ↔ y ∈ x | φ ∧ ψ
7 6 ineqri ⊢ x | φ ∩ x | ψ = x | φ ∧ ψ