This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcim1

Description: Distribution of class substitution over implication. One direction of sbcimg that holds for proper classes. (Contributed by NM, 17-Aug-2018) Avoid ax-10 , ax-12 . (Revised by SN, 26-Oct-2024)

		Ref	Expression
	Assertion	sbcim1	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → 𝐴 ∈ V )
2		dfsbcq2	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) ) )
3		dfsbcq2	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
4		dfsbcq2	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) )
5	3 4	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) ) )
6	2 5	imbi12d	⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ) ↔ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) ) ) )
7		sbi1	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
8	6 7	vtoclg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) ) )
9	1 8	mpcom	⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 → 𝜓 ) → ( [ 𝐴 / 𝑥 ] 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 ) )