Metamath Proof Explorer


Theorem csbriota

Description: Interchange class substitution and restricted description binder. (Contributed by NM, 24-Feb-2013) (Revised by NM, 2-Sep-2018)

Ref Expression
Assertion csbriota A / x ι y B | φ = ι y B | [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 csbeq1 z = A z / x ι y B | φ = A / x ι y B | φ
2 dfsbcq2 z = A z x φ [˙A / x]˙ φ
3 2 riotabidv z = A ι y B | z x φ = ι y B | [˙A / x]˙ φ
4 1 3 eqeq12d z = A z / x ι y B | φ = ι y B | z x φ A / x ι y B | φ = ι y B | [˙A / x]˙ φ
5 vex z V
6 nfs1v x z x φ
7 nfcv _ x B
8 6 7 nfriota _ x ι y B | z x φ
9 sbequ12 x = z φ z x φ
10 9 riotabidv x = z ι y B | φ = ι y B | z x φ
11 5 8 10 csbief z / x ι y B | φ = ι y B | z x φ
12 4 11 vtoclg A V A / x ι y B | φ = ι y B | [˙A / x]˙ φ
13 csbprc ¬ A V A / x ι y B | φ =
14 df-riota ι y B | [˙A / x]˙ φ = ι y | y B [˙A / x]˙ φ
15 euex ∃! y y B [˙A / x]˙ φ y y B [˙A / x]˙ φ
16 sbcex [˙A / x]˙ φ A V
17 16 adantl y B [˙A / x]˙ φ A V
18 17 exlimiv y y B [˙A / x]˙ φ A V
19 15 18 syl ∃! y y B [˙A / x]˙ φ A V
20 iotanul ¬ ∃! y y B [˙A / x]˙ φ ι y | y B [˙A / x]˙ φ =
21 19 20 nsyl5 ¬ A V ι y | y B [˙A / x]˙ φ =
22 14 21 eqtr2id ¬ A V = ι y B | [˙A / x]˙ φ
23 13 22 eqtrd ¬ A V A / x ι y B | φ = ι y B | [˙A / x]˙ φ
24 12 23 pm2.61i A / x ι y B | φ = ι y B | [˙A / x]˙ φ