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

Metamath Proof Explorer

Theorem cbvrab

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvrabw when possible. (Contributed by Andrew Salmon, 11-Jul-2011) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvrab.1 ⊢ Ⅎ _ x A
cbvrab.2 ⊢ Ⅎ _ y A
cbvrab.3 ⊢ Ⅎ y φ
cbvrab.4 ⊢ Ⅎ x ψ
cbvrab.5 ⊢ x = y → φ ↔ ψ
Assertion cbvrab ⊢ x ∈ A | φ = y ∈ A | ψ

Proof

Step Hyp Ref Expression
1 cbvrab.1 ⊢ Ⅎ _ x A
2 cbvrab.2 ⊢ Ⅎ _ y A
3 cbvrab.3 ⊢ Ⅎ y φ
4 cbvrab.4 ⊢ Ⅎ x ψ
5 cbvrab.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 cbvab ⊢ x | x ∈ A ∧ φ = z | z ∈ A ∧ z x φ
14 2 nfcri ⊢ Ⅎ y z ∈ A
15 3 nfsb ⊢ Ⅎ 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 sbie ⊢ 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 cbvab ⊢ 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 | ψ