Metamath Proof Explorer

Theorem axfrege52c

Description: Justification for ax-frege52c . (Contributed by RP, 24-Dec-2019)

Ref Expression
Assertion axfrege52c ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 dfsbcq ⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑥 ] 𝜑 ) )
2 1 biimpd ⊢ ( 𝐴 = 𝐵 → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐵 / 𝑥 ] 𝜑 ) )