Theorem sbabel

Description: Theorem to move a substitution in and out of a class abstraction. (Contributed by NM, 27-Sep-2003) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 28-Oct-2024)

	Ref	Expression
Hypothesis	sbabel.1	⊢ Ⅎ 𝑥 𝐴
Assertion	sbabel	⊢ ( [ 𝑦 / 𝑥 ] { 𝑧 ∣ 𝜑 } ∈ 𝐴 ↔ { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝜑 } ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sbabel.1	⊢ Ⅎ 𝑥 𝐴
2		clabel	⊢ ( { 𝑧 ∣ 𝜑 } ∈ 𝐴 ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) )
3	2	sbbii	⊢ ( [ 𝑦 / 𝑥 ] { 𝑧 ∣ 𝜑 } ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) )
4		sbex	⊢ ( [ 𝑦 / 𝑥 ] ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) ↔ ∃ 𝑣 [ 𝑦 / 𝑥 ] ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) )
5		sban	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) ↔ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) )
6	1	nfcri	⊢ Ⅎ 𝑥 𝑣 ∈ 𝐴
7	6	sbf	⊢ ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴 )
8		sbv	⊢ ( [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ 𝑣 )
9	8	sbrbis	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ↔ ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
10	9	sbalv	⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
11	7 10	anbi12i	⊢ ( ( [ 𝑦 / 𝑥 ] 𝑣 ∈ 𝐴 ∧ [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) ↔ ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
12	5 11	bitri	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) ↔ ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
13	12	exbii	⊢ ( ∃ 𝑣 [ 𝑦 / 𝑥 ] ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ 𝜑 ) ) ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
14	3 4 13	3bitri	⊢ ( [ 𝑦 / 𝑥 ] { 𝑧 ∣ 𝜑 } ∈ 𝐴 ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
15		clabel	⊢ ( { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝜑 } ∈ 𝐴 ↔ ∃ 𝑣 ( 𝑣 ∈ 𝐴 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑣 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
16	14 15	bitr4i	⊢ ( [ 𝑦 / 𝑥 ] { 𝑧 ∣ 𝜑 } ∈ 𝐴 ↔ { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝜑 } ∈ 𝐴 )