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, 26-Dec-2019)

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

Proof

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