Metamath Proof Explorer


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 . (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 sbim ( [ 𝑦 / 𝑧 ] ( 𝑥𝑧𝜑 ) ↔ ( [ 𝑦 / 𝑧 ] 𝑥𝑧 → [ 𝑦 / 𝑧 ] 𝜑 ) )
4 elsb2 ( [ 𝑦 / 𝑧 ] 𝑥𝑧𝑥𝑦 )
5 sbv ( [ 𝑦 / 𝑧 ] 𝜑𝜑 )
6 4 5 imbi12i ( ( [ 𝑦 / 𝑧 ] 𝑥𝑧 → [ 𝑦 / 𝑧 ] 𝜑 ) ↔ ( 𝑥𝑦𝜑 ) )
7 3 6 bitri ( [ 𝑦 / 𝑧 ] ( 𝑥𝑧𝜑 ) ↔ ( 𝑥𝑦𝜑 ) )
8 7 albii ( ∀ 𝑥 [ 𝑦 / 𝑧 ] ( 𝑥𝑧𝜑 ) ↔ ∀ 𝑥 ( 𝑥𝑦𝜑 ) )
9 elequ1 ( 𝑥 = 𝑦 → ( 𝑥𝑧𝑦𝑧 ) )
10 9 1 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑥𝑧𝜑 ) ↔ ( 𝑦𝑧𝜓 ) ) )
11 10 cbvalvw ( ∀ 𝑥 ( 𝑥𝑧𝜑 ) ↔ ∀ 𝑦 ( 𝑦𝑧𝜓 ) )
12 df-ral ( ∀ 𝑦𝑥 𝜓 ↔ ∀ 𝑦 ( 𝑦𝑥𝜓 ) )
13 12 sbbii ( [ 𝑧 / 𝑥 ] ∀ 𝑦𝑥 𝜓 ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦𝑥𝜓 ) )
14 sbal ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ( 𝑦𝑥𝜓 ) ↔ ∀ 𝑦 [ 𝑧 / 𝑥 ] ( 𝑦𝑥𝜓 ) )
15 sbim ( [ 𝑧 / 𝑥 ] ( 𝑦𝑥𝜓 ) ↔ ( [ 𝑧 / 𝑥 ] 𝑦𝑥 → [ 𝑧 / 𝑥 ] 𝜓 ) )
16 elsb2 ( [ 𝑧 / 𝑥 ] 𝑦𝑥𝑦𝑧 )
17 sbv ( [ 𝑧 / 𝑥 ] 𝜓𝜓 )
18 16 17 imbi12i ( ( [ 𝑧 / 𝑥 ] 𝑦𝑥 → [ 𝑧 / 𝑥 ] 𝜓 ) ↔ ( 𝑦𝑧𝜓 ) )
19 15 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 ( ∀ 𝑥𝑦 𝜑 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦𝑥 𝜓 )