Metamath Proof Explorer


Theorem cbvrabcsfw

Description: Version of cbvrabcsf with a disjoint variable condition, which does not require ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 cbvrabcsfw.1 _ y A
2 cbvrabcsfw.2 _ x B
3 cbvrabcsfw.3 y φ
4 cbvrabcsfw.4 x ψ
5 cbvrabcsfw.5 x = y A = B
6 cbvrabcsfw.6 x = y φ ψ
7 nfv z x A φ
8 nfcsb1v _ x z / x A
9 8 nfcri x z z / x A
10 nfs1v x z x φ
11 9 10 nfan x z z / x A z x φ
12 id x = z x = z
13 csbeq1a x = z A = z / x A
14 12 13 eleq12d x = z x A z z / x A
15 sbequ12 x = z φ z x φ
16 14 15 anbi12d x = z x A φ z z / x A z x φ
17 7 11 16 cbvabw x | x A φ = z | z z / x A z x φ
18 nfcv _ y z
19 18 1 nfcsbw _ y z / x A
20 19 nfcri y z z / x A
21 3 nfsbv y z x φ
22 20 21 nfan y z z / x A z x φ
23 nfv z y B ψ
24 id z = y z = y
25 csbeq1 z = y z / x A = y / x A
26 vex y V
27 26 2 5 csbief y / x A = B
28 25 27 eqtrdi z = y z / x A = B
29 24 28 eleq12d z = y z z / x A y B
30 4 6 sbhypf z = y z x φ ψ
31 29 30 anbi12d z = y z z / x A z x φ y B ψ
32 22 23 31 cbvabw z | z z / x A z x φ = y | y B ψ
33 17 32 eqtri x | x A φ = y | y B ψ
34 df-rab x A | φ = x | x A φ
35 df-rab y B | ψ = y | y B ψ
36 33 34 35 3eqtr4i x A | φ = y B | ψ