This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqabi ⊢ 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 | ψ