Theorem cbvral4vw

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

	Ref	Expression
Hypotheses	cbvral4vw.1	|- ( x = a -> ( ph <-> ch ) )
	cbvral4vw.2	|- ( y = b -> ( ch <-> th ) )
	cbvral4vw.3	|- ( z = c -> ( th <-> ta ) )
	cbvral4vw.4	|- ( w = d -> ( ta <-> ps ) )
Assertion	cbvral4vw	|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph <-> A. a e. A A. b e. B A. c e. C A. d e. D ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral4vw.1	|- ( x = a -> ( ph <-> ch ) )
2		cbvral4vw.2	|- ( y = b -> ( ch <-> th ) )
3		cbvral4vw.3	|- ( z = c -> ( th <-> ta ) )
4		cbvral4vw.4	|- ( w = d -> ( ta <-> ps ) )
5	1	ralbidv	|- ( x = a -> ( A. w e. D ph <-> A. w e. D ch ) )
6	2	ralbidv	|- ( y = b -> ( A. w e. D ch <-> A. w e. D th ) )
7	3	ralbidv	|- ( z = c -> ( A. w e. D th <-> A. w e. D ta ) )
8	5 6 7	cbvral3vw	|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph <-> A. a e. A A. b e. B A. c e. C A. w e. D ta )
9	4	cbvralvw	|- ( A. w e. D ta <-> A. d e. D ps )
10	9	3ralbii	|- ( A. a e. A A. b e. B A. c e. C A. w e. D ta <-> A. a e. A A. b e. B A. c e. C A. d e. D ps )
11	8 10	bitri	|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph <-> A. a e. A A. b e. B A. c e. C A. d e. D ps )