Theorem cbvral6vw

Description: Change bound variables of sextuple restricted universal quantification, using implicit substitution. (Contributed by Scott Fenton, 5-Mar-2025)

	Ref	Expression
Hypotheses	cbvral6vw.1	|- ( x = a -> ( ph <-> ch ) )
	cbvral6vw.2	|- ( y = b -> ( ch <-> th ) )
	cbvral6vw.3	|- ( z = c -> ( th <-> ta ) )
	cbvral6vw.4	|- ( w = d -> ( ta <-> et ) )
	cbvral6vw.5	|- ( p = e -> ( et <-> ze ) )
	cbvral6vw.6	|- ( q = f -> ( ze <-> ps ) )
Assertion	cbvral6vw	|- ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ph <-> A. a e. A A. b e. B A. c e. C A. d e. D A. e e. E A. f e. F ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral6vw.1	|- ( x = a -> ( ph <-> ch ) )
2		cbvral6vw.2	|- ( y = b -> ( ch <-> th ) )
3		cbvral6vw.3	|- ( z = c -> ( th <-> ta ) )
4		cbvral6vw.4	|- ( w = d -> ( ta <-> et ) )
5		cbvral6vw.5	|- ( p = e -> ( et <-> ze ) )
6		cbvral6vw.6	|- ( q = f -> ( ze <-> ps ) )
7	1	2ralbidv	|- ( x = a -> ( A. p e. E A. q e. F ph <-> A. p e. E A. q e. F ch ) )
8	2	2ralbidv	|- ( y = b -> ( A. p e. E A. q e. F ch <-> A. p e. E A. q e. F th ) )
9	3	2ralbidv	|- ( z = c -> ( A. p e. E A. q e. F th <-> A. p e. E A. q e. F ta ) )
10	4	2ralbidv	|- ( w = d -> ( A. p e. E A. q e. F ta <-> A. p e. E A. q e. F et ) )
11	7 8 9 10	cbvral4vw	|- ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ph <-> A. a e. A A. b e. B A. c e. C A. d e. D A. p e. E A. q e. F et )
12	5 6	cbvral2vw	|- ( A. p e. E A. q e. F et <-> A. e e. E A. f e. F ps )
13	12	4ralbii	|- ( A. a e. A A. b e. B A. c e. C A. d e. D A. p e. E A. q e. F et <-> A. a e. A A. b e. B A. c e. C A. d e. D A. e e. E A. f e. F ps )
14	11 13	bitri	|- ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F ph <-> A. a e. A A. b e. B A. c e. C A. d e. D A. e e. E A. f e. F ps )