Metamath Proof Explorer


Theorem sbceqbii

Description: Formula-building inference for class substitution. General version of sbcbii . (Contributed by GG, 1-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 sbceqbii.1 𝐴 = 𝐵
2 sbceqbii.2 ( 𝜑𝜓 )
3 2 abbii { 𝑥𝜑 } = { 𝑥𝜓 }
4 1 3 eleq12i ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝐵 ∈ { 𝑥𝜓 } )
5 df-sbc ( [ 𝐴 / 𝑥 ] 𝜑𝐴 ∈ { 𝑥𝜑 } )
6 df-sbc ( [ 𝐵 / 𝑥 ] 𝜓𝐵 ∈ { 𝑥𝜓 } )
7 4 5 6 3bitr4i ( [ 𝐴 / 𝑥 ] 𝜑[ 𝐵 / 𝑥 ] 𝜓 )