csbopabgALT

Description: Move substitution into a class abstraction. Version of csbopab with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007) (Proof shortened by Mario Carneiro, 17-Nov-2016) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	csbopabgALT	$⊢ A \in V \to ⦋ A / x ⦌ \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} φ\}$

Proof

Step	Hyp	Ref	Expression
1		csbeq1	$⊢ w = A \to ⦋ w / x ⦌ \{⟨y, z⟩ \| φ\} = ⦋ A / x ⦌ \{⟨y, z⟩ \| φ\}$
2		dfsbcq2	$⊢ w = A \to ([w/ x] φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$
3	2	opabbidv	$⊢ w = A \to \{⟨y, z⟩ \| [w/ x] φ\} = \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} φ\}$
4	1 3	eqeq12d	$⊢ w = A \to (⦋ w / x ⦌ \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| [w/ x] φ\} \leftrightarrow ⦋ A / x ⦌ \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} φ\})$
5		vex	$⊢ w \in V$
6		nfs1v	$⊢ Ⅎ x [w/ x] φ$
7	6	nfopab	$⊢ \underline{Ⅎ} x \{⟨y, z⟩ \| [w/ x] φ\}$
8		sbequ12	$⊢ x = w \to (φ \leftrightarrow [w/ x] φ)$
9	8	opabbidv	$⊢ x = w \to \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| [w/ x] φ\}$
10	5 7 9	csbief	$⊢ ⦋ w / x ⦌ \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| [w/ x] φ\}$
11	4 10	vtoclg	$⊢ A \in V \to ⦋ A / x ⦌ \{⟨y, z⟩ \| φ\} = \{⟨y, z⟩ \| \underset{˙}{[} A / x \underset{˙}{]} φ\}$

Metamath Proof Explorer

Theorem csbopabgALT

Proof