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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( [ 𝐴 / 𝑥 ] 𝜓 → [ 𝐴 / 𝑥 ] 𝜒 ) )