Metamath Proof Explorer


Theorem sbcg

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024)

Ref Expression
Assertion sbcg AV[˙A/x]˙φφ

Proof

Step Hyp Ref Expression
1 df-sbc [˙A/x]˙φAx|φ
2 dfclel Ax|φyy=Ayx|φ
3 df-clab yx|φyxφ
4 sbv yxφφ
5 3 4 bitri yx|φφ
6 5 anbi2i y=Ayx|φy=Aφ
7 6 exbii yy=Ayx|φyy=Aφ
8 1 2 7 3bitrri yy=Aφ[˙A/x]˙φ
9 dfclel AVyy=AyV
10 9 biimpi AVyy=AyV
11 simpr y=Aφφ
12 11 ax-gen yy=Aφφ
13 19.23v yy=Aφφyy=Aφφ
14 13 biimpi yy=Aφφyy=Aφφ
15 12 14 mp1i yy=AyVyy=Aφφ
16 2a1 y=AyVφy=A
17 16 imp y=AyVφy=A
18 17 ancrd y=AyVφy=Aφ
19 18 eximi yy=AyVyφy=Aφ
20 19.37imv yφy=Aφφyy=Aφ
21 19 20 syl yy=AyVφyy=Aφ
22 15 21 impbid yy=AyVyy=Aφφ
23 10 22 syl AVyy=Aφφ
24 8 23 bitr3id AV[˙A/x]˙φφ