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 ⊢ [˙A / x]˙ ∃! y ∈ B φ ↔ ∃! y ∈ B [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ ∃! y ∈ B φ → A ∈ V
2 reurex ⊢ ∃! y ∈ B [˙A / x]˙ φ → ∃ y ∈ B [˙A / x]˙ φ
3 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
4 3 rexlimivw ⊢ ∃ y ∈ B [˙A / x]˙ φ → A ∈ V
5 2 4 syl ⊢ ∃! y ∈ B [˙A / x]˙ φ → A ∈ V
6 dfsbcq2 ⊢ z = A → z x ∃! y ∈ B φ ↔ [˙A / x]˙ ∃! y ∈ B φ
7 dfsbcq2 ⊢ z = A → z x φ ↔ [˙A / x]˙ φ
8 7 reubidv ⊢ z = A → ∃! y ∈ B z x φ ↔ ∃! y ∈ B [˙A / x]˙ φ
9 nfcv ⊢ Ⅎ _ x B
10 nfs1v ⊢ Ⅎ x z x φ
11 9 10 nfreuw ⊢ Ⅎ x ∃! y ∈ B z x φ
12 sbequ12 ⊢ x = z → φ ↔ z x φ
13 12 reubidv ⊢ x = z → ∃! y ∈ B φ ↔ ∃! y ∈ B z x φ
14 11 13 sbiev ⊢ z x ∃! y ∈ B φ ↔ ∃! y ∈ B z x φ
15 6 8 14 vtoclbg ⊢ A ∈ V → [˙A / x]˙ ∃! y ∈ B φ ↔ ∃! y ∈ B [˙A / x]˙ φ
16 1 5 15 pm5.21nii ⊢ [˙A / x]˙ ∃! y ∈ B φ ↔ ∃! y ∈ B [˙A / x]˙ φ