Metamath Proof Explorer


Theorem cbvrabw

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvrabw.1 _ x A
cbvrabw.2 _ y A
cbvrabw.3 y φ
cbvrabw.4 x ψ
cbvrabw.5 x = y φ ψ
Assertion cbvrabw x A | φ = y A | ψ

Proof

Step Hyp Ref Expression
1 cbvrabw.1 _ x A
2 cbvrabw.2 _ y A
3 cbvrabw.3 y φ
4 cbvrabw.4 x ψ
5 cbvrabw.5 x = y φ ψ
6 nfv z x A φ
7 1 nfcri x z A
8 nfs1v x z x φ
9 7 8 nfan x z A z x φ
10 eleq1w x = z x A z A
11 sbequ12 x = z φ z x φ
12 10 11 anbi12d x = z x A φ z A z x φ
13 6 9 12 cbvabw x | x A φ = z | z A z x φ
14 2 nfcri y z A
15 3 nfsbv y z x φ
16 14 15 nfan y z A z x φ
17 nfv z y A ψ
18 eleq1w z = y z A y A
19 sbequ z = y z x φ y x φ
20 4 5 sbiev y x φ ψ
21 19 20 bitrdi z = y z x φ ψ
22 18 21 anbi12d z = y z A z x φ y A ψ
23 16 17 22 cbvabw z | z A z x φ = y | y A ψ
24 13 23 eqtri x | x A φ = y | y A ψ
25 df-rab x A | φ = x | x A φ
26 df-rab y A | ψ = y | y A ψ
27 24 25 26 3eqtr4i x A | φ = y A | ψ