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

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 GG, 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 | ψ