csbie2g

Description: Conversion of implicit substitution to explicit class substitution. This version of csbie avoids a disjointness condition on x , A and x , D by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016)

	Ref	Expression
Hypotheses	csbie2g.1	$⊢ x = y \to B = C$
	csbie2g.2	$⊢ y = A \to C = D$
Assertion	csbie2g	$⊢ A \in V \to ⦋ A / x ⦌ B = D$

Proof

Step	Hyp	Ref	Expression
1		csbie2g.1	$⊢ x = y \to B = C$
2		csbie2g.2	$⊢ y = A \to C = D$
3		df-csb	$⊢ ⦋ A / x ⦌ B = \{z \| \underset{˙}{[} A / x \underset{˙}{]} z \in B\}$
4	1	eleq2d	$⊢ x = y \to (z \in B \leftrightarrow z \in C)$
5	2	eleq2d	$⊢ y = A \to (z \in C \leftrightarrow z \in D)$
6	4 5	sbcie2g	$⊢ A \in V \to (\underset{˙}{[} A / x \underset{˙}{]} z \in B \leftrightarrow z \in D)$
7	6	eqabcdv	$⊢ A \in V \to \{z \| \underset{˙}{[} A / x \underset{˙}{]} z \in B\} = D$
8	3 7	eqtrid	$⊢ A \in V \to ⦋ A / x ⦌ B = D$

Metamath Proof Explorer

Theorem csbie2g

Proof