Metamath Proof Explorer


Theorem cbvrabcsf

Description: A more general version of cbvrab with no distinct variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralcsf.1 _ y A
2 cbvralcsf.2 _ x B
3 cbvralcsf.3 y φ
4 cbvralcsf.4 x ψ
5 cbvralcsf.5 x = y A = B
6 cbvralcsf.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 cbvab x | x A φ = z | z z / x A z x φ
18 nfcv _ y z
19 18 1 nfcsb _ y z / x A
20 19 nfcri y z z / x A
21 3 nfsb 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 df-csb y / x A = v | [˙y / x]˙ v A
27 2 nfcri x v B
28 5 eleq2d x = y v A v B
29 27 28 sbie y x v A v B
30 sbsbc y x v A [˙y / x]˙ v A
31 29 30 bitr3i v B [˙y / x]˙ v A
32 31 abbi2i B = v | [˙y / x]˙ v A
33 26 32 eqtr4i y / x A = B
34 25 33 eqtrdi z = y z / x A = B
35 24 34 eleq12d z = y z z / x A y B
36 sbequ z = y z x φ y x φ
37 4 6 sbie y x φ ψ
38 36 37 bitrdi z = y z x φ ψ
39 35 38 anbi12d z = y z z / x A z x φ y B ψ
40 22 23 39 cbvab z | z z / x A z x φ = y | y B ψ
41 17 40 eqtri x | x A φ = y | y B ψ
42 df-rab x A | φ = x | x A φ
43 df-rab y B | ψ = y | y B ψ
44 41 42 43 3eqtr4i x A | φ = y B | ψ