Metamath Proof Explorer

Theorem cbvralfwOLD

Description: Obsolete version of cbvralfw as of 23-May-2024. (Contributed by NM, 7-Mar-2004) (Revised by Gino Giotto, 10-Jan-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvralfwOLD.1 ⊢ Ⅎ _ x A
2 cbvralfwOLD.2 ⊢ Ⅎ _ y A
3 cbvralfwOLD.3 ⊢ Ⅎ y φ
4 cbvralfwOLD.4 ⊢ Ⅎ x ψ
5 cbvralfwOLD.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 nfsbv ⊢ Ⅎ 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 sbiev ⊢ 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 ψ