Theorem bdsepnft 9342

Description: Closed form of bdsepnf 9343. Version of ax-bdsep 9339 with one DV condition removed, the other DV condition replaced by a non-freeness antecedent, and without initial universal quantifier. Use bdsep1 9340 when sufficient. (Contributed by BJ, 19-Oct-2019.)

Hypothesis

Ref	Expression
bdsepnft.1	⊢ BOUNDED φ

Assertion

Ref	Expression
bdsepnft	⊢ (∀xℲ𝑏φ → ∃𝑏∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ)))

Distinct variable group:   𝑎,𝑏,x

Allowed substitution hints:   φ(x,𝑎,𝑏)

Proof of Theorem bdsepnft

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bdsepnft.1	. . 3 ⊢ BOUNDED φ
2	1	bdsep2 9341	. 2 ⊢ ∃y∀x(x ∈ y ↔ (x ∈ 𝑎 ∧ φ))
3		nfnf1 1433	. . . 4 ⊢ Ⅎ𝑏Ⅎ𝑏φ
4	3	nfal 1465	. . 3 ⊢ Ⅎ𝑏∀xℲ𝑏φ
5		nfa1 1431	. . . 4 ⊢ Ⅎx∀xℲ𝑏φ
6		nfvd 1419	. . . . 5 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏 x ∈ y)
7		nfv 1418	. . . . . . 7 ⊢ Ⅎ𝑏 x ∈ 𝑎
8	7	a1i 9	. . . . . 6 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏 x ∈ 𝑎)
9		sp 1398	. . . . . 6 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏φ)
10	8, 9	nfand 1457	. . . . 5 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏(x ∈ 𝑎 ∧ φ))
11	6, 10	nfbid 1477	. . . 4 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏(x ∈ y ↔ (x ∈ 𝑎 ∧ φ)))
12	5, 11	nfald 1640	. . 3 ⊢ (∀xℲ𝑏φ → Ⅎ𝑏∀x(x ∈ y ↔ (x ∈ 𝑎 ∧ φ)))
13		nfv 1418	. . . . . 6 ⊢ Ⅎx y = 𝑏
14	5, 13	nfan 1454	. . . . 5 ⊢ Ⅎx(∀xℲ𝑏φ ∧ y = 𝑏)
15		elequ2 1598	. . . . . . 7 ⊢ (y = 𝑏 → (x ∈ y ↔ x ∈ 𝑏))
16	15	adantl 262	. . . . . 6 ⊢ ((∀xℲ𝑏φ ∧ y = 𝑏) → (x ∈ y ↔ x ∈ 𝑏))
17	16	bibi1d 222	. . . . 5 ⊢ ((∀xℲ𝑏φ ∧ y = 𝑏) → ((x ∈ y ↔ (x ∈ 𝑎 ∧ φ)) ↔ (x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ))))
18	14, 17	albid 1503	. . . 4 ⊢ ((∀xℲ𝑏φ ∧ y = 𝑏) → (∀x(x ∈ y ↔ (x ∈ 𝑎 ∧ φ)) ↔ ∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ))))
19	18	ex 108	. . 3 ⊢ (∀xℲ𝑏φ → (y = 𝑏 → (∀x(x ∈ y ↔ (x ∈ 𝑎 ∧ φ)) ↔ ∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ)))))
20	4, 12, 19	cbvexd 1799	. 2 ⊢ (∀xℲ𝑏φ → (∃y∀x(x ∈ y ↔ (x ∈ 𝑎 ∧ φ)) ↔ ∃𝑏∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ))))
21	2, 20	mpbii 136	1 ⊢ (∀xℲ𝑏φ → ∃𝑏∀x(x ∈ 𝑏 ↔ (x ∈ 𝑎 ∧ φ)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1240  Ⅎwnf 1346  ∃wex 1378  BOUNDED wbd 9267

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-bdsep 9339

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-cleq 2030  df-clel 2033

This theorem is referenced by:  bdsepnf  9343