sbcie3s

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

	Ref	Expression
Hypotheses	sbcie3s.a	$⊢ A = E (W)$
	sbcie3s.b	$⊢ B = F (W)$
	sbcie3s.c	$⊢ C = G (W)$
	sbcie3s.1	$⊢ (a = A \land b = B \land c = C) \to (φ \leftrightarrow ψ)$
Assertion	sbcie3s	$⊢ w = W \to (\underset{˙}{[} E (w) / a \underset{˙}{]} \underset{˙}{[} F (w) / b \underset{˙}{]} \underset{˙}{[} G (w) / c \underset{˙}{]} ψ \leftrightarrow φ)$

Proof

Step	Hyp	Ref	Expression
1		sbcie3s.a	$⊢ A = E (W)$
2		sbcie3s.b	$⊢ B = F (W)$
3		sbcie3s.c	$⊢ C = G (W)$
4		sbcie3s.1	$⊢ (a = A \land b = B \land c = C) \to (φ \leftrightarrow ψ)$
5		fvexd	$⊢ w = W \to E (w) \in V$
6		fvexd	$⊢ (w = W \land a = E (w)) \to F (w) \in V$
7		fvexd	$⊢ ((w = W \land a = E (w)) \land b = F (w)) \to G (w) \in V$
8		simpllr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to a = E (w)$
9		fveq2	$⊢ w = W \to E (w) = E (W)$
10	9	ad3antrrr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to E (w) = E (W)$
11	8 10	eqtrd	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to a = E (W)$
12	11 1	eqtr4di	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to a = A$
13		simplr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to b = F (w)$
14		fveq2	$⊢ w = W \to F (w) = F (W)$
15	14	ad3antrrr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to F (w) = F (W)$
16	13 15	eqtrd	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to b = F (W)$
17	16 2	eqtr4di	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to b = B$
18		simpr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to c = G (w)$
19		fveq2	$⊢ w = W \to G (w) = G (W)$
20	19	ad3antrrr	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to G (w) = G (W)$
21	18 20	eqtrd	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to c = G (W)$
22	21 3	eqtr4di	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to c = C$
23	12 17 22 4	syl3anc	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to (φ \leftrightarrow ψ)$
24	23	bicomd	$⊢ (((w = W \land a = E (w)) \land b = F (w)) \land c = G (w)) \to (ψ \leftrightarrow φ)$
25	7 24	sbcied	$⊢ ((w = W \land a = E (w)) \land b = F (w)) \to (\underset{˙}{[} G (w) / c \underset{˙}{]} ψ \leftrightarrow φ)$
26	6 25	sbcied	$⊢ (w = W \land a = E (w)) \to (\underset{˙}{[} F (w) / b \underset{˙}{]} \underset{˙}{[} G (w) / c \underset{˙}{]} ψ \leftrightarrow φ)$
27	5 26	sbcied	$⊢ w = W \to (\underset{˙}{[} E (w) / a \underset{˙}{]} \underset{˙}{[} F (w) / b \underset{˙}{]} \underset{˙}{[} G (w) / c \underset{˙}{]} ψ \leftrightarrow φ)$

Metamath Proof Explorer

Theorem sbcie3s

Proof