Metamath Proof Explorer

Theorem wl-dfrabf

Description: Alternate definition of restricted class abstraction ( df-wl-rab ), when x is not free in A . (Contributed by Wolf Lammen, 29-May-2023)

Ref Expression
Assertion wl-dfrabf ⊢ Ⅎ _ x A → x : A | φ = x | x ∈ A ∧ φ

Proof

Step Hyp Ref Expression
1 wl-dfrabsb ⊢ x : A | φ = y | y ∈ A ∧ y x φ
2 nfnfc1 ⊢ Ⅎ x Ⅎ _ x A
3 id ⊢ Ⅎ _ x A → Ⅎ _ x A
4 2 3 wl-clelsb3df ⊢ Ⅎ _ x A → z x x ∈ A ↔ z ∈ A
5 clelsb3 ⊢ z y y ∈ A ↔ z ∈ A
6 4 5 syl6rbbr ⊢ Ⅎ _ x A → z y y ∈ A ↔ z x x ∈ A
7 sbco2vv ⊢ z y y x φ ↔ z x φ
8 7 a1i ⊢ Ⅎ _ x A → z y y x φ ↔ z x φ
9 6 8 anbi12d ⊢ Ⅎ _ x A → z y y ∈ A ∧ z y y x φ ↔ z x x ∈ A ∧ z x φ
10 df-clab ⊢ z ∈ y | y ∈ A ∧ y x φ ↔ z y y ∈ A ∧ y x φ
11 sban ⊢ z y y ∈ A ∧ y x φ ↔ z y y ∈ A ∧ z y y x φ
12 10 11 bitri ⊢ z ∈ y | y ∈ A ∧ y x φ ↔ z y y ∈ A ∧ z y y x φ
13 df-clab ⊢ z ∈ x | x ∈ A ∧ φ ↔ z x x ∈ A ∧ φ
14 sban ⊢ z x x ∈ A ∧ φ ↔ z x x ∈ A ∧ z x φ
15 13 14 bitri ⊢ z ∈ x | x ∈ A ∧ φ ↔ z x x ∈ A ∧ z x φ
16 9 12 15 3bitr4g ⊢ Ⅎ _ x A → z ∈ y | y ∈ A ∧ y x φ ↔ z ∈ x | x ∈ A ∧ φ
17 16 eqrdv ⊢ Ⅎ _ x A → y | y ∈ A ∧ y x φ = x | x ∈ A ∧ φ
18 1 17 syl5eq ⊢ Ⅎ _ x A → x : A | φ = x | x ∈ A ∧ φ