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

Metamath Proof Explorer

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 )