This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( [ 𝐴 / 𝑥 ] ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 )