Metamath Proof Explorer

Theorem sbcabel

Description: Interchange class substitution and class abstraction. (Contributed by NM, 5-Nov-2005)

Ref Expression
Hypothesis sbcabel.1 ⊢ Ⅎ 𝑥 𝐵
Assertion sbcabel ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝜑 } ∈ 𝐵 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sbcabel.1 ⊢ Ⅎ 𝑥 𝐵
2 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
3 sbcex2 ⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑤 [ 𝐴 / 𝑥 ] ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) )
4 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑤 = { 𝑦 ∣ 𝜑 } ∧ [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ) )
5 sbcal ⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) )
6 sbcbig ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
7 sbcg ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤 ) )
8 7 bibi1d ⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
9 6 8 bitrd ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) ↔ ( 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
10 9 albidv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 [ 𝐴 / 𝑥 ] ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
11 5 10 bitrid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) )
12 abeq2 ⊢ ( 𝑤 = { 𝑦 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) )
13 12 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] 𝑤 = { 𝑦 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ 𝜑 ) )
14 abeq2 ⊢ ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑤 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
15 11 13 14 3bitr4g ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑤 = { 𝑦 ∣ 𝜑 } ↔ 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ) )
16 1 nfcri ⊢ Ⅎ 𝑥 𝑤 ∈ 𝐵
17 16 sbcgf ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵 ) )
18 15 17 anbi12d ⊢ ( 𝐴 ∈ V → ( ( [ 𝐴 / 𝑥 ] 𝑤 = { 𝑦 ∣ 𝜑 } ∧ [ 𝐴 / 𝑥 ] 𝑤 ∈ 𝐵 ) ↔ ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ) )
19 4 18 bitrid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ↔ ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ) )
20 19 exbidv ⊢ ( 𝐴 ∈ V → ( ∃ 𝑤 [ 𝐴 / 𝑥 ] ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ) )
21 3 20 bitrid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∧ 𝑤 ∈ 𝐵 ) ) )
22 dfclel ⊢ ( { 𝑦 ∣ 𝜑 } ∈ 𝐵 ↔ ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) )
23 22 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝜑 } ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ 𝜑 } ∧ 𝑤 ∈ 𝐵 ) )
24 dfclel ⊢ ( { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∈ 𝐵 ↔ ∃ 𝑤 ( 𝑤 = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∧ 𝑤 ∈ 𝐵 ) )
25 21 23 24 3bitr4g ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝜑 } ∈ 𝐵 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∈ 𝐵 ) )
26 2 25 syl ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] { 𝑦 ∣ 𝜑 } ∈ 𝐵 ↔ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ∈ 𝐵 ) )