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

Metamath Proof Explorer

Theorem sbcie3s

Description: A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses sbcie3s.a ⊢ 𝐴 = ( 𝐸 ‘ 𝑊 )
sbcie3s.b ⊢ 𝐵 = ( 𝐹 ‘ 𝑊 )
sbcie3s.c ⊢ 𝐶 = ( 𝐺 ‘ 𝑊 )
sbcie3s.1 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion sbcie3s ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] [ ( 𝐹 ‘ 𝑤 ) / 𝑏 ] [ ( 𝐺 ‘ 𝑤 ) / 𝑐 ] 𝜓 ↔ 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbcie3s.a ⊢ 𝐴 = ( 𝐸 ‘ 𝑊 )
2 sbcie3s.b ⊢ 𝐵 = ( 𝐹 ‘ 𝑊 )
3 sbcie3s.c ⊢ 𝐶 = ( 𝐺 ‘ 𝑊 )
4 sbcie3s.1 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶 ) → ( 𝜑 ↔ 𝜓 ) )
5 fvexd ⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) ∈ V )
6 fvexd ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ V )
7 fvexd ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ V )
8 simpllr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑎 = ( 𝐸 ‘ 𝑤 ) )
9 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑊 ) )
10 9 ad3antrrr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐸 ‘ 𝑤 ) = ( 𝐸 ‘ 𝑊 ) )
11 8 10 eqtrd ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑎 = ( 𝐸 ‘ 𝑊 ) )
12 11 1 eqtr4di ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑎 = 𝐴 )
13 simplr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑏 = ( 𝐹 ‘ 𝑤 ) )
14 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑊 ) )
15 14 ad3antrrr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑊 ) )
16 13 15 eqtrd ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑏 = ( 𝐹 ‘ 𝑊 ) )
17 16 2 eqtr4di ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑏 = 𝐵 )
18 simpr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑐 = ( 𝐺 ‘ 𝑤 ) )
19 fveq2 ⊢ ( 𝑤 = 𝑊 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑊 ) )
20 19 ad3antrrr ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑊 ) )
21 18 20 eqtrd ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑐 = ( 𝐺 ‘ 𝑊 ) )
22 21 3 eqtr4di ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → 𝑐 = 𝐶 )
23 12 17 22 4 syl3anc ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → ( 𝜑 ↔ 𝜓 ) )
24 23 bicomd ⊢ ( ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) ∧ 𝑐 = ( 𝐺 ‘ 𝑤 ) ) → ( 𝜓 ↔ 𝜑 ) )
25 7 24 sbcied ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) ∧ 𝑏 = ( 𝐹 ‘ 𝑤 ) ) → ( [ ( 𝐺 ‘ 𝑤 ) / 𝑐 ] 𝜓 ↔ 𝜑 ) )
26 6 25 sbcied ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = ( 𝐸 ‘ 𝑤 ) ) → ( [ ( 𝐹 ‘ 𝑤 ) / 𝑏 ] [ ( 𝐺 ‘ 𝑤 ) / 𝑐 ] 𝜓 ↔ 𝜑 ) )
27 5 26 sbcied ⊢ ( 𝑤 = 𝑊 → ( [ ( 𝐸 ‘ 𝑤 ) / 𝑎 ] [ ( 𝐹 ‘ 𝑤 ) / 𝑏 ] [ ( 𝐺 ‘ 𝑤 ) / 𝑐 ] 𝜓 ↔ 𝜑 ) )