Theorem sbcimdv

Description: Substitution analogue of Theorem 19.20 of Margaris p. 90 ( alim ). (Contributed by NM, 11-Nov-2005) (Revised by NM, 17-Aug-2018) (Proof shortened by JJ, 7-Jul-2021) Reduce axiom usage. (Revised by GG, 12-Oct-2024)

	Ref	Expression
Hypothesis	sbcimdv.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	sbcimdv	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		sbcimdv.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜓 } )
3		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜓 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
4		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
5	4	anbi2i	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
6	5	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
7	2 3 6	3bitri	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
8	7	biimpi	⊢ ( [ 𝐴 / 𝑥 ] 𝜓 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) )
9	1	sbimdv	⊢ ( 𝜑 → ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜒 ) )
10	9	anim2d	⊢ ( 𝜑 → ( ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ) )
11	10	eximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜓 ) → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ) )
12		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜒 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜒 } )
13		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜒 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) )
14		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜒 } ↔ [ 𝑦 / 𝑥 ] 𝜒 )
15	14	anbi2i	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) ↔ ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) )
16	15	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜒 } ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) )
17	12 13 16	3bitrri	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) ↔ [ 𝐴 / 𝑥 ] 𝜒 )
18	17	biimpi	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ [ 𝑦 / 𝑥 ] 𝜒 ) → [ 𝐴 / 𝑥 ] 𝜒 )
19	8 11 18	syl56	⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) )