| 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 ) ) |