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