Theorem strcollnft 10109

Description: Closed form of strcollnf 10110. Version of ax-strcoll 10107 with one DV condition removed, the other DV condition replaced by a non-freeness antecedent, and without initial universal quantifier. (Contributed by BJ, 21-Oct-2019.)

Assertion

Ref	Expression
strcollnft	⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))

Distinct variable group:   𝑎,𝑏,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem strcollnft

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		strcoll2 10108	. 2 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
2		nfnf1 1436	. . . . 5 ⊢ Ⅎ𝑏Ⅎ𝑏𝜑
3	2	nfal 1468	. . . 4 ⊢ Ⅎ𝑏∀𝑦Ⅎ𝑏𝜑
4	3	nfal 1468	. . 3 ⊢ Ⅎ𝑏∀𝑥∀𝑦Ⅎ𝑏𝜑
5		nfa2 1471	. . . 4 ⊢ Ⅎ𝑦∀𝑥∀𝑦Ⅎ𝑏𝜑
6		nfvd 1422	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏 𝑦 ∈ 𝑧)
7		nfa1 1434	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥Ⅎ𝑏𝜑
8		nfcvd 2179	. . . . . . . 8 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏𝑎)
9		sp 1401	. . . . . . . 8 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
10	7, 8, 9	nfrexdxy 2357	. . . . . . 7 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
11	10	sps 1430	. . . . . 6 ⊢ (∀𝑦∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
12	11	alcoms 1365	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
13	6, 12	nfbid 1480	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
14	5, 13	nfald 1643	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
15		nfv 1421	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝑏
16	5, 15	nfan 1457	. . . . 5 ⊢ Ⅎ𝑦(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
17		elequ2 1601	. . . . . . 7 ⊢ (𝑧 = 𝑏 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
18	17	adantl 262	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
19	18	bibi1d 222	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ (𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
20	16, 19	albid 1506	. . . 4 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
21	20	ex 108	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (𝑧 = 𝑏 → (∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))))
22	4, 14, 21	cbvexd 1802	. 2 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
23	1, 22	syl5ib 143	1 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241  Ⅎwnf 1349  ∃wex 1381  ∀wral 2306  ∃wrex 2307

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-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-strcoll 10107

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312

This theorem is referenced by:  strcollnf  10110