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 ⊢ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ

Proof

Step Hyp Ref Expression
1 sbcimdv.1 ⊢ φ → ψ → χ
2 df-sbc ⊢ [˙A / x]˙ ψ ↔ A ∈ x | ψ
3 dfclel ⊢ A ∈ x | ψ ↔ ∃ y y = A ∧ y ∈ x | ψ
4 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
5 4 anbi2i ⊢ y = A ∧ y ∈ x | ψ ↔ y = A ∧ y x ψ
6 5 exbii ⊢ ∃ y y = A ∧ y ∈ x | ψ ↔ ∃ y y = A ∧ y x ψ
7 2 3 6 3bitri ⊢ [˙A / x]˙ ψ ↔ ∃ y y = A ∧ y x ψ
8 7 biimpi ⊢ [˙A / x]˙ ψ → ∃ y y = A ∧ y x ψ
9 1 sbimdv ⊢ φ → y x ψ → y x χ
10 9 anim2d ⊢ φ → y = A ∧ y x ψ → y = A ∧ y x χ
11 10 eximdv ⊢ φ → ∃ y y = A ∧ y x ψ → ∃ y y = A ∧ y x χ
12 df-sbc ⊢ [˙A / x]˙ χ ↔ A ∈ x | χ
13 dfclel ⊢ A ∈ x | χ ↔ ∃ y y = A ∧ y ∈ x | χ
14 df-clab ⊢ y ∈ x | χ ↔ y x χ
15 14 anbi2i ⊢ y = A ∧ y ∈ x | χ ↔ y = A ∧ y x χ
16 15 exbii ⊢ ∃ y y = A ∧ y ∈ x | χ ↔ ∃ y y = A ∧ y x χ
17 12 13 16 3bitrri ⊢ ∃ y y = A ∧ y x χ ↔ [˙A / x]˙ χ
18 17 biimpi ⊢ ∃ y y = A ∧ y x χ → [˙A / x]˙ χ
19 8 11 18 syl56 ⊢ φ → [˙A / x]˙ ψ → [˙A / x]˙ χ