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

Metamath Proof Explorer

Theorem sbcssg

Description: Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012) (Proof shortened by Alexander van der Vekens, 23-Jul-2017)

		Ref	Expression
	Assertion	sbcssg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 ⊆ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcal	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
2		sbcimg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ) )
3		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 )
4		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5	3 4	imbi12i	⊢ ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
6	2 5	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ↔ ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
7	6	albidv	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
8	1 7	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
9		df-ss	⊢ ( 𝐵 ⊆ 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
10	9	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 ⊆ 𝐶 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶 ) )
11		df-ss	⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ ∀ 𝑦 ( 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → 𝑦 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )
12	8 10 11	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 ⊆ 𝐶 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ⊆ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )