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 φ A x | ψ B x | χ
5 df-sbc [˙A / x]˙ ψ A x | ψ
6 df-sbc [˙B / x]˙ χ B x | χ
7 4 5 6 3bitr4g φ [˙A / x]˙ ψ [˙B / x]˙ χ