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 φxyz|ψ=xyz|χ

Proof

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