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

Metamath Proof Explorer

Theorem sbralieOLD

Description: Obsolete version of sbralie as of 13-Nov-2025. (Contributed by NM, 5-Sep-2004) (Proof modification is discouraged.) (New usage is discouraged.)

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

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 ⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )