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]˙∃!yBφ∃!yB[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 sbcex [˙A/x]˙∃!yBφAV
2 reurex ∃!yB[˙A/x]˙φyB[˙A/x]˙φ
3 sbcex [˙A/x]˙φAV
4 3 rexlimivw yB[˙A/x]˙φAV
5 2 4 syl ∃!yB[˙A/x]˙φAV
6 dfsbcq2 z=Azx∃!yBφ[˙A/x]˙∃!yBφ
7 dfsbcq2 z=Azxφ[˙A/x]˙φ
8 7 reubidv z=A∃!yBzxφ∃!yB[˙A/x]˙φ
9 nfcv _xB
10 nfs1v xzxφ
11 9 10 nfreuw x∃!yBzxφ
12 sbequ12 x=zφzxφ
13 12 reubidv x=z∃!yBφ∃!yBzxφ
14 11 13 sbiev zx∃!yBφ∃!yBzxφ
15 6 8 14 vtoclbg AV[˙A/x]˙∃!yBφ∃!yB[˙A/x]˙φ
16 1 5 15 pm5.21nii [˙A/x]˙∃!yBφ∃!yB[˙A/x]˙φ