sbcies

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

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

Step	Hyp	Ref	Expression
1		sbcies.a	$⊢ A = E (W)$
2		sbcies.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
3		fvexd	$⊢ w = W \to E (w) \in V$
4		simpr	$⊢ (w = W \land a = E (w)) \to a = E (w)$
5		fveq2	$⊢ w = W \to E (w) = E (W)$
6	1 5	eqtr4id	$⊢ w = W \to A = E (w)$
7	6	adantr	$⊢ (w = W \land a = E (w)) \to A = E (w)$
8	4 7	eqtr4d	$⊢ (w = W \land a = E (w)) \to a = A$
9	8 2	syl	$⊢ (w = W \land a = E (w)) \to (φ \leftrightarrow ψ)$
10	9	bicomd	$⊢ (w = W \land a = E (w)) \to (ψ \leftrightarrow φ)$
11	3 10	sbcied	$⊢ w = W \to (\underset{˙}{[} E (w) / a \underset{˙}{]} ψ \leftrightarrow φ)$

Metamath Proof Explorer