Theorem csbeq12dv

Description: Formula-building inference for class substitution. (Contributed by SN, 3-Nov-2023)

	Ref	Expression
Hypotheses	csbeq12dv.1	⊢ ( 𝜑 → 𝐴 = 𝐶 )
	csbeq12dv.2	⊢ ( 𝜑 → 𝐵 = 𝐷 )
Assertion	csbeq12dv	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		csbeq12dv.1	⊢ ( 𝜑 → 𝐴 = 𝐶 )
2		csbeq12dv.2	⊢ ( 𝜑 → 𝐵 = 𝐷 )
3	1	csbeq1d	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
4	2	csbeq2dv	⊢ ( 𝜑 → ⦋ 𝐶 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐷 )
5	3 4	eqtrd	⊢ ( 𝜑 → ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐷 )