Theorem abbibw

Description: Replace ax-10 , ax-11 , ax-12 in abbib with substitution hypotheses. (Contributed by SN, 27-May-2025)

	Ref	Expression
Hypotheses	abbibw.ph	|- ( x = y -> ( ph <-> th ) )
	abbibw.ps	|- ( x = y -> ( ps <-> ch ) )
Assertion	abbibw	|- ( { x | ph } = { x | ps } <-> A. x ( ph <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		abbibw.ph	|- ( x = y -> ( ph <-> th ) )
2		abbibw.ps	|- ( x = y -> ( ps <-> ch ) )
3		dfcleq	|- ( { x | ph } = { x | ps } <-> A. y ( y e. { x | ph } <-> y e. { x | ps } ) )
4		vex	|- y e. _V
5	4 1	elab	|- ( y e. { x | ph } <-> th )
6	4 2	elab	|- ( y e. { x | ps } <-> ch )
7	5 6	bibi12i	|- ( ( y e. { x | ph } <-> y e. { x | ps } ) <-> ( th <-> ch ) )
8	7	albii	|- ( A. y ( y e. { x | ph } <-> y e. { x | ps } ) <-> A. y ( th <-> ch ) )
9	1 2	bibi12d	|- ( x = y -> ( ( ph <-> ps ) <-> ( th <-> ch ) ) )
10	9	bicomd	|- ( x = y -> ( ( th <-> ch ) <-> ( ph <-> ps ) ) )
11	10	equcoms	|- ( y = x -> ( ( th <-> ch ) <-> ( ph <-> ps ) ) )
12	11	cbvalvw	|- ( A. y ( th <-> ch ) <-> A. x ( ph <-> ps ) )
13	3 8 12	3bitri	|- ( { x | ph } = { x | ps } <-> A. x ( ph <-> ps ) )