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	⊢ Ⅎ 𝑥 𝐴
	cbvralfwOLD.2	⊢ Ⅎ 𝑦 𝐴
	cbvralfwOLD.3	⊢ Ⅎ 𝑦 𝜑
	cbvralfwOLD.4	⊢ Ⅎ 𝑥 𝜓
	cbvralfwOLD.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	cbvralfwOLD	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cbvralfwOLD.1	⊢ Ⅎ 𝑥 𝐴
2		cbvralfwOLD.2	⊢ Ⅎ 𝑦 𝐴
3		cbvralfwOLD.3	⊢ Ⅎ 𝑦 𝜑
4		cbvralfwOLD.4	⊢ Ⅎ 𝑥 𝜓
5		cbvralfwOLD.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 → 𝜑 )
7	1	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
8		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
9	7 8	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
10		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
11		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
12	10 11	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ) )
13	6 9 12	cbvalv1	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) )
14	2	nfcri	⊢ Ⅎ 𝑦 𝑧 ∈ 𝐴
15	3	nfsbv	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] 𝜑
16	14 15	nfim	⊢ Ⅎ 𝑦 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 )
17		nfv	⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐴 → 𝜓 )
18		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
19		sbequ	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
20	4 5	sbiev	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
21	19 20	bitrdi	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
22	18 21	imbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜓 ) ) )
23	16 17 22	cbvalv1	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐴 → [ 𝑧 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
24	13 23	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
25		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
26		df-ral	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → 𝜓 ) )
27	24 25 26	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )