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

Metamath Proof Explorer

Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralf.1 ⊢ Ⅎ _ x A
2 cbvralf.2 ⊢ Ⅎ _ y A
3 cbvralf.3 ⊢ Ⅎ y φ
4 cbvralf.4 ⊢ Ⅎ x ψ
5 cbvralf.5 ⊢ x = y → φ ↔ ψ
6 nfv ⊢ Ⅎ z x ∈ A → φ
7 1 nfcri ⊢ Ⅎ x z ∈ A
8 nfs1v ⊢ Ⅎ x z x φ
9 7 8 nfim ⊢ Ⅎ x z ∈ A → z x φ
10 eleq1w ⊢ x = z → x ∈ A ↔ z ∈ A
11 sbequ12 ⊢ x = z → φ ↔ z x φ
12 10 11 imbi12d ⊢ x = z → x ∈ A → φ ↔ z ∈ A → z x φ
13 6 9 12 cbvalv1 ⊢ ∀ x x ∈ A → φ ↔ ∀ z z ∈ A → z x φ
14 2 nfcri ⊢ Ⅎ y z ∈ A
15 3 nfsb ⊢ Ⅎ y z x φ
16 14 15 nfim ⊢ Ⅎ 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 imbi12d ⊢ z = y → z ∈ A → z x φ ↔ y ∈ A → ψ
23 16 17 22 cbvalv1 ⊢ ∀ z z ∈ A → z x φ ↔ ∀ y y ∈ A → ψ
24 13 23 bitri ⊢ ∀ x x ∈ A → φ ↔ ∀ y y ∈ A → ψ
25 df-ral ⊢ ∀ x ∈ A φ ↔ ∀ x x ∈ A → φ
26 df-ral ⊢ ∀ y ∈ A ψ ↔ ∀ y y ∈ A → ψ
27 24 25 26 3bitr4i ⊢ ∀ x ∈ A φ ↔ ∀ y ∈ A ψ