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 GG, 12-Oct-2024)

	Ref	Expression
Assertion	sbcg	|- ( A e. V -> ( [. A / x ]. ph <-> ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-sbc	|- ( [. A / x ]. ph <-> A e. { x | ph } )
2		dfclel	|- ( A e. { x | ph } <-> E. y ( y = A /\ y e. { x | ph } ) )
3		df-clab	|- ( y e. { x | ph } <-> [ y / x ] ph )
4		sbv	|- ( [ y / x ] ph <-> ph )
5	3 4	bitri	|- ( y e. { x | ph } <-> ph )
6	5	anbi2i	|- ( ( y = A /\ y e. { x | ph } ) <-> ( y = A /\ ph ) )
7	6	exbii	|- ( E. y ( y = A /\ y e. { x | ph } ) <-> E. y ( y = A /\ ph ) )
8	1 2 7	3bitrri	|- ( E. y ( y = A /\ ph ) <-> [. A / x ]. ph )
9		dfclel	|- ( A e. V <-> E. y ( y = A /\ y e. V ) )
10	9	biimpi	|- ( A e. V -> E. y ( y = A /\ y e. V ) )
11		simpr	|- ( ( y = A /\ ph ) -> ph )
12	11	ax-gen	|- A. y ( ( y = A /\ ph ) -> ph )
13		19.23v	|- ( A. y ( ( y = A /\ ph ) -> ph ) <-> ( E. y ( y = A /\ ph ) -> ph ) )
14	13	biimpi	|- ( A. y ( ( y = A /\ ph ) -> ph ) -> ( E. y ( y = A /\ ph ) -> ph ) )
15	12 14	mp1i	|- ( E. y ( y = A /\ y e. V ) -> ( E. y ( y = A /\ ph ) -> ph ) )
16		2a1	|- ( y = A -> ( y e. V -> ( ph -> y = A ) ) )
17	16	imp	|- ( ( y = A /\ y e. V ) -> ( ph -> y = A ) )
18	17	ancrd	|- ( ( y = A /\ y e. V ) -> ( ph -> ( y = A /\ ph ) ) )
19	18	eximi	|- ( E. y ( y = A /\ y e. V ) -> E. y ( ph -> ( y = A /\ ph ) ) )
20		19.37imv	|- ( E. y ( ph -> ( y = A /\ ph ) ) -> ( ph -> E. y ( y = A /\ ph ) ) )
21	19 20	syl	|- ( E. y ( y = A /\ y e. V ) -> ( ph -> E. y ( y = A /\ ph ) ) )
22	15 21	impbid	|- ( E. y ( y = A /\ y e. V ) -> ( E. y ( y = A /\ ph ) <-> ph ) )
23	10 22	syl	|- ( A e. V -> ( E. y ( y = A /\ ph ) <-> ph ) )
24	8 23	bitr3id	|- ( A e. V -> ( [. A / x ]. ph <-> ph ) )