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	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		csbeq1	⊢ ( 𝑤 = 𝐴 → ⦋ 𝑤 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } )
2		dfsbcq2	⊢ ( 𝑤 = 𝐴 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
3	2	opabbidv	⊢ ( 𝑤 = 𝐴 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝑤 / 𝑥 ] 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )
4	1 3	eqeq12d	⊢ ( 𝑤 = 𝐴 → ( ⦋ 𝑤 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝑤 / 𝑥 ] 𝜑 } ↔ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } ) )
5		vex	⊢ 𝑤 ∈ V
6		nfs1v	⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
7	6	nfopab	⊢ Ⅎ 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝑤 / 𝑥 ] 𝜑 }
8		sbequ12	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
9	8	opabbidv	⊢ ( 𝑥 = 𝑤 → { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝑤 / 𝑥 ] 𝜑 } )
10	5 7 9	csbief	⊢ ⦋ 𝑤 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝑤 / 𝑥 ] 𝜑 }
11	4 10	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )

Metamath Proof Explorer

Theorem csbopabgALT

Proof