Theorem sbralie

Description: Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004) Avoid ax-ext , df-cleq , df-clel . (Revised by Wolf Lammen, 10-Mar-2025)

	Ref	Expression
Hypothesis	sbralie.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	sbralie	⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbralie.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) )
3		nfv	⊢ Ⅎ 𝑧 𝜑
4	3	sblim	⊢ ( [ 𝑦 / 𝑧 ] ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ( [ 𝑦 / 𝑧 ] 𝑥 ∈ 𝑧 → 𝜑 ) )
5		elsb2	⊢ ( [ 𝑦 / 𝑧 ] 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦 )
6	5	imbi1i	⊢ ( ( [ 𝑦 / 𝑧 ] 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 → 𝜑 ) )
7	4 6	bitri	⊢ ( [ 𝑦 / 𝑧 ] ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ( 𝑥 ∈ 𝑦 → 𝜑 ) )
8	7	albii	⊢ ( ∀ 𝑥 [ 𝑦 / 𝑧 ] ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → 𝜑 ) )
9		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
10	9 1	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ( 𝑦 ∈ 𝑧 → 𝜓 ) ) )
11	10	cbvalvw	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝜓 ) )
12		df-ral	⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝜓 ) )
13	12	sbbii	⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝜓 ) )
14		sbal	⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝜓 ) ↔ ∀ 𝑦 [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝑥 → 𝜓 ) )
15		nfv	⊢ Ⅎ 𝑥 𝜓
16	15	sblim	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝑥 → 𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 → 𝜓 ) )
17		elsb2	⊢ ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑧 )
18	17	imbi1i	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑦 ∈ 𝑥 → 𝜓 ) ↔ ( 𝑦 ∈ 𝑧 → 𝜓 ) )
19	16 18	bitri	⊢ ( [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝑥 → 𝜓 ) ↔ ( 𝑦 ∈ 𝑧 → 𝜓 ) )
20	19	albii	⊢ ( ∀ 𝑦 [ 𝑧 / 𝑥 ] ( 𝑦 ∈ 𝑥 → 𝜓 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝜓 ) )
21	13 14 20	3bitrri	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 → 𝜓 ) ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )
22	11 21	bitri	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )
23	22	sbbii	⊢ ( [ 𝑦 / 𝑧 ] ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ [ 𝑦 / 𝑧 ] [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )
24		sbal	⊢ ( [ 𝑦 / 𝑧 ] ∀ 𝑥 ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ ∀ 𝑥 [ 𝑦 / 𝑧 ] ( 𝑥 ∈ 𝑧 → 𝜑 ) )
25		sbco2vv	⊢ ( [ 𝑦 / 𝑧 ] [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )
26	23 24 25	3bitr3i	⊢ ( ∀ 𝑥 [ 𝑦 / 𝑧 ] ( 𝑥 ∈ 𝑧 → 𝜑 ) ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )
27	2 8 26	3bitr2i	⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )