Metamath Proof Explorer


Theorem sbceqbid

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

Ref Expression
Hypotheses sbceqbid.1 ( 𝜑𝐴 = 𝐵 )
sbceqbid.2 ( 𝜑 → ( 𝜓𝜒 ) )
Assertion sbceqbid ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓[ 𝐵 / 𝑥 ] 𝜒 ) )

Proof

Step Hyp Ref Expression
1 sbceqbid.1 ( 𝜑𝐴 = 𝐵 )
2 sbceqbid.2 ( 𝜑 → ( 𝜓𝜒 ) )
3 2 abbidv ( 𝜑 → { 𝑥𝜓 } = { 𝑥𝜒 } )
4 1 3 eleq12d ( 𝜑 → ( 𝐴 ∈ { 𝑥𝜓 } ↔ 𝐵 ∈ { 𝑥𝜒 } ) )
5 df-sbc ( [ 𝐴 / 𝑥 ] 𝜓𝐴 ∈ { 𝑥𝜓 } )
6 df-sbc ( [ 𝐵 / 𝑥 ] 𝜒𝐵 ∈ { 𝑥𝜒 } )
7 4 5 6 3bitr4g ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓[ 𝐵 / 𝑥 ] 𝜒 ) )