Theorem strcollnft 10779

Description: Closed form of strcollnf 10780. Version of ax-strcoll 10777 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 10778	. 2 ⊢ (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
2		nfnf1 1476	. . . . 5 ⊢ Ⅎ𝑏Ⅎ𝑏𝜑
3	2	nfal 1508	. . . 4 ⊢ Ⅎ𝑏∀𝑦Ⅎ𝑏𝜑
4	3	nfal 1508	. . 3 ⊢ Ⅎ𝑏∀𝑥∀𝑦Ⅎ𝑏𝜑
5		nfa2 1511	. . . 4 ⊢ Ⅎ𝑦∀𝑥∀𝑦Ⅎ𝑏𝜑
6		nfvd 1462	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏 𝑦 ∈ 𝑧)
7		nfa1 1474	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥Ⅎ𝑏𝜑
8		nfcvd 2220	. . . . . . . 8 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏𝑎)
9		sp 1441	. . . . . . . 8 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏𝜑)
10	7, 8, 9	nfrexdxy 2399	. . . . . . 7 ⊢ (∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
11	10	sps 1470	. . . . . 6 ⊢ (∀𝑦∀𝑥Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
12	11	alcoms 1405	. . . . 5 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∃𝑥 ∈ 𝑎 𝜑)
13	6, 12	nfbid 1520	. . . 4 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
14	5, 13	nfald 1683	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → Ⅎ𝑏∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑))
15		nfv 1461	. . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝑏
16	5, 15	nfan 1497	. . . . 5 ⊢ Ⅎ𝑦(∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏)
17		elequ2 1641	. . . . . . 7 ⊢ (𝑧 = 𝑏 → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
18	17	adantl 271	. . . . . 6 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (𝑦 ∈ 𝑧 ↔ 𝑦 ∈ 𝑏))
19	18	bibi1d 231	. . . . 5 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → ((𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ (𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
20	16, 19	albid 1546	. . . 4 ⊢ ((∀𝑥∀𝑦Ⅎ𝑏𝜑 ∧ 𝑧 = 𝑏) → (∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
21	20	ex 113	. . 3 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (𝑧 = 𝑏 → (∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑))))
22	4, 14, 21	cbvexd 1843	. 2 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∃𝑧∀𝑦(𝑦 ∈ 𝑧 ↔ ∃𝑥 ∈ 𝑎 𝜑) ↔ ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))
23	1, 22	syl5ib 152	1 ⊢ (∀𝑥∀𝑦Ⅎ𝑏𝜑 → (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏∀𝑦(𝑦 ∈ 𝑏 ↔ ∃𝑥 ∈ 𝑎 𝜑)))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103  ∀wal 1282  Ⅎwnf 1389  ∃wex 1421  ∀wral 2348  ∃wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-strcoll 10777

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354

This theorem is referenced by:  strcollnf  10780