Metamath Proof Explorer


Theorem sbceqbid

Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018)

Ref Expression
Hypotheses sbceqbid.1 φA=B
sbceqbid.2 φψχ
Assertion sbceqbid φ[˙A/x]˙ψ[˙B/x]˙χ

Proof

Step Hyp Ref Expression
1 sbceqbid.1 φA=B
2 sbceqbid.2 φψχ
3 2 abbidv φx|ψ=x|χ
4 1 3 eleq12d φAx|ψBx|χ
5 df-sbc [˙A/x]˙ψAx|ψ
6 df-sbc [˙B/x]˙χBx|χ
7 4 5 6 3bitr4g φ[˙A/x]˙ψ[˙B/x]˙χ