Metamath Proof Explorer

Theorem sbcie2s

Description: A special version of class substitution commonly used for structures. (Contributed by Thierry Arnoux, 14-Mar-2019) (Revised by SN, 2-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		sbcie2s.a	$⊢ A = E (W)$
2		sbcie2s.b	$⊢ B = F (W)$
3		sbcie2s.1	$⊢ (a = A \land b = B) \to (φ \leftrightarrow ψ)$
4		fvex	$⊢ E (w) \in V$
5		fvex	$⊢ F (w) \in V$
6		fveq2	$⊢ w = W \to E (w) = E (W)$
7	6 1	eqtr4di	$⊢ w = W \to E (w) = A$
8	7	eqeq2d	$⊢ w = W \to (a = E (w) \leftrightarrow a = A)$
9	8	biimpd	$⊢ w = W \to (a = E (w) \to a = A)$
10		fveq2	$⊢ w = W \to F (w) = F (W)$
11	10 2	eqtr4di	$⊢ w = W \to F (w) = B$
12	11	eqeq2d	$⊢ w = W \to (b = F (w) \leftrightarrow b = B)$
13	12	biimpd	$⊢ w = W \to (b = F (w) \to b = B)$
14	3	a1i	$⊢ w = W \to ((a = A \land b = B) \to (φ \leftrightarrow ψ))$
15	9 13 14	syl2and	$⊢ w = W \to ((a = E (w) \land b = F (w)) \to (φ \leftrightarrow ψ))$
16	4 5 15	sbc2iedv	$⊢ w = W \to (\underset{˙}{[} E (w) / a \underset{˙}{]} \underset{˙}{[} F (w) / b \underset{˙}{]} φ \leftrightarrow ψ)$