This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cbvral8vw

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

		Ref	Expression
	Hypotheses	cbvral8vw.1	\|- ( x = a -> ( ph <-> ch ) )
		cbvral8vw.2	\|- ( y = b -> ( ch <-> th ) )
		cbvral8vw.3	\|- ( z = c -> ( th <-> ta ) )
		cbvral8vw.4	\|- ( w = d -> ( ta <-> et ) )
		cbvral8vw.5	\|- ( p = e -> ( et <-> ze ) )
		cbvral8vw.6	\|- ( q = f -> ( ze <-> si ) )
		cbvral8vw.7	\|- ( r = g -> ( si <-> rh ) )
		cbvral8vw.8	\|- ( s = h -> ( rh <-> ps ) )
	Assertion	cbvral8vw	\|- ( A. x e. A A. y e. B A. z e. C A. w e. D A. p e. E A. q e. F A. r e. G A. s e. H 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 A. g e. G A. h e. H ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral8vw.1	\|- ( x = a -> ( ph <-> ch ) )
2		cbvral8vw.2	\|- ( y = b -> ( ch <-> th ) )
3		cbvral8vw.3	\|- ( z = c -> ( th <-> ta ) )
4		cbvral8vw.4	\|- ( w = d -> ( ta <-> et ) )
5		cbvral8vw.5	\|- ( p = e -> ( et <-> ze ) )
6		cbvral8vw.6	\|- ( q = f -> ( ze <-> si ) )
7		cbvral8vw.7	\|- ( r = g -> ( si <-> rh ) )
8		cbvral8vw.8	\|- ( s = h -> ( rh <-> ps ) )
9	1	4ralbidv	\|- ( x = a -> ( A. p e. E A. q e. F A. r e. G A. s e. H ph <-> A. p e. E A. q e. F A. r e. G A. s e. H ch ) )
10	2	4ralbidv	\|- ( y = b -> ( A. p e. E A. q e. F A. r e. G A. s e. H ch <-> A. p e. E A. q e. F A. r e. G A. s e. H th ) )
11	3	4ralbidv	\|- ( z = c -> ( A. p e. E A. q e. F A. r e. G A. s e. H th <-> A. p e. E A. q e. F A. r e. G A. s e. H ta ) )
12	4	4ralbidv	\|- ( w = d -> ( A. p e. E A. q e. F A. r e. G A. s e. H ta <-> A. p e. E A. q e. F A. r e. G A. s e. H et ) )
13	9 10 11 12	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 A. r e. G A. s e. H 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 A. r e. G A. s e. H et )
14	5 6 7 8	cbvral4vw	\|- ( A. p e. E A. q e. F A. r e. G A. s e. H et <-> A. e e. E A. f e. F A. g e. G A. h e. H ps )
15	14	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 A. r e. G A. s e. H 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 A. g e. G A. h e. H ps )
16	13 15	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 A. r e. G A. s e. H 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 A. g e. G A. h e. H ps )