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 Gino Giotto, 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]˙ψAx|ψ
3 dfclel Ax|ψyy=Ayx|ψ
4 df-clab yx|ψyxψ
5 4 anbi2i y=Ayx|ψy=Ayxψ
6 5 exbii yy=Ayx|ψyy=Ayxψ
7 2 3 6 3bitri [˙A/x]˙ψyy=Ayxψ
8 7 biimpi [˙A/x]˙ψyy=Ayxψ
9 1 sbimdv φyxψyxχ
10 9 anim2d φy=Ayxψy=Ayxχ
11 10 eximdv φyy=Ayxψyy=Ayxχ
12 df-sbc [˙A/x]˙χAx|χ
13 dfclel Ax|χyy=Ayx|χ
14 df-clab yx|χyxχ
15 14 anbi2i y=Ayx|χy=Ayxχ
16 15 exbii yy=Ayx|χyy=Ayxχ
17 12 13 16 3bitrri yy=Ayxχ[˙A/x]˙χ
18 17 biimpi yy=Ayxχ[˙A/x]˙χ
19 8 11 18 syl56 φ[˙A/x]˙ψ[˙A/x]˙χ