Metamath Proof Explorer

Theorem nfabdw

Description: Bound-variable hypothesis builder for a class abstraction. Version of nfabd with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 8-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses nfabdw.1 ⊢ Ⅎ y φ
nfabdw.2 ⊢ φ → Ⅎ x ψ
Assertion nfabdw ⊢ φ → Ⅎ _ x y | ψ

Proof

Step Hyp Ref Expression
1 nfabdw.1 ⊢ Ⅎ y φ
2 nfabdw.2 ⊢ φ → Ⅎ x ψ
3 nfv ⊢ Ⅎ z φ
4 df-clab ⊢ z ∈ y | ψ ↔ z y ψ
5 1 2 alrimi ⊢ φ → ∀ y Ⅎ x ψ
6 nfa1 ⊢ Ⅎ y ∀ y Ⅎ x ψ
7 sb6 ⊢ z y ψ ↔ ∀ y y = z → ψ
8 7 a1i ⊢ ∀ y Ⅎ x ψ → z y ψ ↔ ∀ y y = z → ψ
9 7 biimpri ⊢ ∀ y y = z → ψ → z y ψ
10 9 axc4i ⊢ ∀ y y = z → ψ → ∀ y z y ψ
11 8 10 syl6bi ⊢ ∀ y Ⅎ x ψ → z y ψ → ∀ y z y ψ
12 6 11 nf5d ⊢ ∀ y Ⅎ x ψ → Ⅎ y z y ψ
13 6 12 nfim1 ⊢ Ⅎ y ∀ y Ⅎ x ψ → z y ψ
14 sbequ12 ⊢ y = z → ψ ↔ z y ψ
15 14 imbi2d ⊢ y = z → ∀ y Ⅎ x ψ → ψ ↔ ∀ y Ⅎ x ψ → z y ψ
16 13 15 equsalv ⊢ ∀ y y = z → ∀ y Ⅎ x ψ → ψ ↔ ∀ y Ⅎ x ψ → z y ψ
17 16 bicomi ⊢ ∀ y Ⅎ x ψ → z y ψ ↔ ∀ y y = z → ∀ y Ⅎ x ψ → ψ
18 nfv ⊢ Ⅎ x y = z
19 nfnf1 ⊢ Ⅎ x Ⅎ x ψ
20 19 nfal ⊢ Ⅎ x ∀ y Ⅎ x ψ
21 sp ⊢ ∀ y Ⅎ x ψ → Ⅎ x ψ
22 20 21 nfim1 ⊢ Ⅎ x ∀ y Ⅎ x ψ → ψ
23 18 22 nfim ⊢ Ⅎ x y = z → ∀ y Ⅎ x ψ → ψ
24 23 nfal ⊢ Ⅎ x ∀ y y = z → ∀ y Ⅎ x ψ → ψ
25 17 24 nfxfr ⊢ Ⅎ x ∀ y Ⅎ x ψ → z y ψ
26 pm5.5 ⊢ ∀ y Ⅎ x ψ → ∀ y Ⅎ x ψ → z y ψ ↔ z y ψ
27 20 26 nfbidf ⊢ ∀ y Ⅎ x ψ → Ⅎ x ∀ y Ⅎ x ψ → z y ψ ↔ Ⅎ x z y ψ
28 25 27 mpbii ⊢ ∀ y Ⅎ x ψ → Ⅎ x z y ψ
29 5 28 syl ⊢ φ → Ⅎ x z y ψ
30 4 29 nfxfrd ⊢ φ → Ⅎ x z ∈ y | ψ
31 3 30 nfcd ⊢ φ → Ⅎ _ x y | ψ