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

Metamath Proof Explorer

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 )