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

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, 28-Oct-2024)

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 clabel ⊢ z | φ ∈ A ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ
3 2 sbbii ⊢ y x z | φ ∈ A ↔ y x ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ
4 sbex ⊢ y x ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ ∃ v y x v ∈ A ∧ ∀ z z ∈ v ↔ φ
5 sban ⊢ y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ y x v ∈ A ∧ y x ∀ z z ∈ v ↔ φ
6 1 nfcri ⊢ Ⅎ x v ∈ A
7 6 sbf ⊢ y x v ∈ A ↔ v ∈ A
8 sbv ⊢ y x z ∈ v ↔ z ∈ v
9 8 sbrbis ⊢ y x z ∈ v ↔ φ ↔ z ∈ v ↔ y x φ
10 9 sbalv ⊢ y x ∀ z z ∈ v ↔ φ ↔ ∀ z z ∈ v ↔ y x φ
11 7 10 anbi12i ⊢ y x v ∈ A ∧ y x ∀ z z ∈ v ↔ φ ↔ v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
12 5 11 bitri ⊢ y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
13 12 exbii ⊢ ∃ v y x v ∈ A ∧ ∀ z z ∈ v ↔ φ ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
14 3 4 13 3bitri ⊢ y x z | φ ∈ A ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
15 clabel ⊢ z | y x φ ∈ A ↔ ∃ v v ∈ A ∧ ∀ z z ∈ v ↔ y x φ
16 14 15 bitr4i ⊢ y x z | φ ∈ A ↔ z | y x φ ∈ A