Metamath Proof Explorer


Theorem oprabbid

Description: Equivalent wff's yield equal operation class abstractions (deduction form). (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses oprabbid.1 x φ
oprabbid.2 y φ
oprabbid.3 z φ
oprabbid.4 φ ψ χ
Assertion oprabbid φ x y z | ψ = x y z | χ

Proof

Step Hyp Ref Expression
1 oprabbid.1 x φ
2 oprabbid.2 y φ
3 oprabbid.3 z φ
4 oprabbid.4 φ ψ χ
5 4 anbi2d φ w = x y z ψ w = x y z χ
6 3 5 exbid φ z w = x y z ψ z w = x y z χ
7 2 6 exbid φ y z w = x y z ψ y z w = x y z χ
8 1 7 exbid φ x y z w = x y z ψ x y z w = x y z χ
9 8 abbidv φ w | x y z w = x y z ψ = w | x y z w = x y z χ
10 df-oprab x y z | ψ = w | x y z w = x y z ψ
11 df-oprab x y z | χ = w | x y z w = x y z χ
12 9 10 11 3eqtr4g φ x y z | ψ = x y z | χ