Metamath Proof Explorer

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 ⊢ Ⅎ _ x A
Assertion sbabel ⊢ y x z | φ ∈ A ↔ z | y x φ ∈ A

Proof

Step Hyp Ref Expression
1 sbabel.1 ⊢ Ⅎ _ x A
2 sbex ⊢ y x ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ ∃ v y x v ∈ A ∧ ∀ z z ∈ v ↔ φ
3 sban ⊢ y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ y x v ∈ A ∧ y x ∀ z z ∈ v ↔ φ
4 1 nfcri ⊢ Ⅎ x v ∈ A
5 4 sbf ⊢ y x v ∈ A ↔ v ∈ A
6 nfv ⊢ Ⅎ x z ∈ v
7 6 sbf ⊢ y x z ∈ v ↔ z ∈ v
8 7 sbrbis ⊢ y x z ∈ v ↔ φ ↔ z ∈ v ↔ y x φ
9 8 sbalv ⊢ y x ∀ z z ∈ v ↔ φ ↔ ∀ z z ∈ v ↔ y x φ
10 5 9 anbi12i ⊢ y x v ∈ A ∧ y x ∀ z z ∈ v ↔ φ ↔ v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
11 3 10 bitri ⊢ y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
12 11 exbii ⊢ ∃ v y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
13 2 12 bitri ⊢ y x ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
14 clabel ⊢ z | φ ∈ A ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ
15 14 sbbii ⊢ y x z | φ ∈ A ↔ y x ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ
16 clabel ⊢ z | y x φ ∈ A ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
17 13 15 16 3bitr4i ⊢ y x z | φ ∈ A ↔ z | y x φ ∈ A