csbopab

Description: Move substitution into a class abstraction. Version of csbopabgALT without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007) (Revised by NM, 23-Aug-2018)

		Ref	Expression
	Assertion	csbopab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 }

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	⊢ ( 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )
12		csbprc	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = ∅ )
13		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
14	13	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ [ 𝐴 / 𝑥 ] 𝜑 )
15	14	nexdv	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑧 [ 𝐴 / 𝑥 ] 𝜑 )
16	15	nexdv	⊢ ( ¬ 𝐴 ∈ V → ¬ ∃ 𝑦 ∃ 𝑧 [ 𝐴 / 𝑥 ] 𝜑 )
17		opabn0	⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑧 [ 𝐴 / 𝑥 ] 𝜑 )
18	17	necon1bbii	⊢ ( ¬ ∃ 𝑦 ∃ 𝑧 [ 𝐴 / 𝑥 ] 𝜑 ↔ { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } = ∅ )
19	16 18	sylib	⊢ ( ¬ 𝐴 ∈ V → { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } = ∅ )
20	12 19	eqtr4d	⊢ ( ¬ 𝐴 ∈ V → ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 } )
21	11 20	pm2.61i	⊢ ⦋ 𝐴 / 𝑥 ⦌ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ [ 𝐴 / 𝑥 ] 𝜑 }

Metamath Proof Explorer

Theorem csbopab

Proof