Metamath Proof Explorer

Theorem rabrab

Description: Abstract builder restricted to another restricted abstract builder. (Contributed by Thierry Arnoux, 30-Aug-2017)

Ref Expression
Assertion rabrab ⊢ x ∈ x ∈ A | φ | ψ = x ∈ A | φ ∧ ψ

Proof

Step Hyp Ref Expression
1 rabid ⊢ x ∈ x ∈ A | φ ↔ x ∈ A ∧ φ
2 1 anbi1i ⊢ x ∈ x ∈ A | φ ∧ ψ ↔ x ∈ A ∧ φ ∧ ψ
3 anass ⊢ x ∈ A ∧ φ ∧ ψ ↔ x ∈ A ∧ φ ∧ ψ
4 2 3 bitri ⊢ x ∈ x ∈ A | φ ∧ ψ ↔ x ∈ A ∧ φ ∧ ψ
5 4 rabbia2 ⊢ x ∈ x ∈ A | φ | ψ = x ∈ A | φ ∧ ψ