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

Metamath Proof Explorer

Theorem sbralieALT

Description: Alternative shorter proof of sbralie dependent on ax-ext , df-cleq , df-clel . (Contributed by NM, 5-Sep-2004) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 sbralie.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 cbvralsvw ⊢ ( ∀ 𝑦 ∈ 𝑥 𝜓 ↔ ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
3 2 sbbii ⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 )
4 raleq ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 ) )
5 4 sbievw ⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑧 ∈ 𝑥 [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 )
6 cbvralsvw ⊢ ( ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝑦 [ 𝑥 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜓 )
7 sbco2vv ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜓 ↔ [ 𝑥 / 𝑦 ] 𝜓 )
8 1 bicomd ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
9 8 equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜑 ) )
10 9 sbievw ⊢ ( [ 𝑥 / 𝑦 ] 𝜓 ↔ 𝜑 )
11 7 10 bitri ⊢ ( [ 𝑥 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜓 ↔ 𝜑 )
12 11 ralbii ⊢ ( ∀ 𝑥 ∈ 𝑦 [ 𝑥 / 𝑧 ] [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝑦 𝜑 )
13 6 12 bitri ⊢ ( ∀ 𝑧 ∈ 𝑦 [ 𝑧 / 𝑦 ] 𝜓 ↔ ∀ 𝑥 ∈ 𝑦 𝜑 )
14 3 5 13 3bitrri ⊢ ( ∀ 𝑥 ∈ 𝑦 𝜑 ↔ [ 𝑦 / 𝑥 ] ∀ 𝑦 ∈ 𝑥 𝜓 )