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

Metamath Proof Explorer

Theorem sbcralt

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008) (Revised by David Abernethy, 22-Feb-2010)

Ref Expression
Assertion sbcralt ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 sbccow ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 )
2 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) → 𝐴 ∈ 𝑉 )
3 sbsbc ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 )
4 nfcv ⊢ Ⅎ 𝑥 𝐵
5 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝜑
6 4 5 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑
7 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
8 7 ralbidv ⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ) )
9 6 8 sbiev ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
10 3 9 bitr3i ⊢ ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 )
11 nfnfc1 ⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝐴
12 nfcvd ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 𝑧 )
13 id ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 𝐴 )
14 12 13 nfeqd ⊢ ( Ⅎ 𝑦 𝐴 → Ⅎ 𝑦 𝑧 = 𝐴 )
15 11 14 nfan1 ⊢ Ⅎ 𝑦 ( Ⅎ 𝑦 𝐴 ∧ 𝑧 = 𝐴 )
16 dfsbcq2 ⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
17 16 adantl ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝑧 = 𝐴 ) → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
18 15 17 ralbid ⊢ ( ( Ⅎ 𝑦 𝐴 ∧ 𝑧 = 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
19 18 adantll ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) ∧ 𝑧 = 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
20 10 19 bitrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) ∧ 𝑧 = 𝐴 ) → ( [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
21 2 20 sbcied ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) → ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )
22 1 21 bitr3id ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Ⅎ 𝑦 𝐴 ) → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑦 ∈ 𝐵 [ 𝐴 / 𝑥 ] 𝜑 ) )