Theorem sbcreu

Description: Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcreu	⊢ ( [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 → 𝐴 ∈ V )
2		reurex	⊢ ( ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 → ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )
3		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
4	3	rexlimivw	⊢ ( ∃ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
5	2 4	syl	⊢ ( ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
6		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ) )
7		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
8	7	reubidv	⊢ ( 𝑧 = 𝐴 → ( ∃! 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
9		nfcv	⊢ Ⅎ 𝑥 𝐵
10		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
11	9 10	nfreuw	⊢ Ⅎ 𝑥 ∃! 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑
12		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
13	12	reubidv	⊢ ( 𝑥 = 𝑧 → ( ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ) )
14	11 13	sbiev	⊢ ( [ 𝑧 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
15	6 8 14	vtoclbg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
16	1 5 15	pm5.21nii	⊢ ( [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )