Theorem nfvres 5545

Description: The value of a non-member of a restriction is the empty set. (Contributed by NM, 13-Nov-1995.)

Assertion

Ref	Expression
nfvres	⊢ (¬ 𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = ∅)

Proof of Theorem nfvres

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fv 5221	. . . . . . . . . 10 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥)
2		df-iota 5175	. . . . . . . . . 10 ⊢ (℩𝑥𝐴(𝐹 ↾ 𝐵)𝑥) = ∪ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}}
3	1, 2	eqtri 2198	. . . . . . . . 9 ⊢ ((𝐹 ↾ 𝐵)‘𝐴) = ∪ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}}
4	3	eleq2i 2244	. . . . . . . 8 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) ↔ 𝑧 ∈ ∪ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}})
5		eluni 3811	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}} ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}}))
6	4, 5	bitri 184	. . . . . . 7 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) ↔ ∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}}))
7		exsimpr 1618	. . . . . . 7 ⊢ (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}}) → ∃𝑤 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}})
8	6, 7	sylbi 121	. . . . . 6 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) → ∃𝑤 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}})
9		df-clab 2164	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}} ↔ [𝑤 / 𝑦]{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦})
10		nfv 1528	. . . . . . . . 9 ⊢ Ⅎ𝑦{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤}
11		sneq 3603	. . . . . . . . . 10 ⊢ (𝑦 = 𝑤 → {𝑦} = {𝑤})
12	11	eqeq2d 2189	. . . . . . . . 9 ⊢ (𝑦 = 𝑤 → ({𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦} ↔ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤}))
13	10, 12	sbie 1791	. . . . . . . 8 ⊢ ([𝑤 / 𝑦]{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦} ↔ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤})
14	9, 13	bitri 184	. . . . . . 7 ⊢ (𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}} ↔ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤})
15	14	exbii 1605	. . . . . 6 ⊢ (∃𝑤 𝑤 ∈ {𝑦 ∣ {𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑦}} ↔ ∃𝑤{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤})
16	8, 15	sylib 122	. . . . 5 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) → ∃𝑤{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤})
17		euabsn2 3661	. . . . 5 ⊢ (∃!𝑥 𝐴(𝐹 ↾ 𝐵)𝑥 ↔ ∃𝑤{𝑥 ∣ 𝐴(𝐹 ↾ 𝐵)𝑥} = {𝑤})
18	16, 17	sylibr 134	. . . 4 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) → ∃!𝑥 𝐴(𝐹 ↾ 𝐵)𝑥)
19		euex 2056	. . . 4 ⊢ (∃!𝑥 𝐴(𝐹 ↾ 𝐵)𝑥 → ∃𝑥 𝐴(𝐹 ↾ 𝐵)𝑥)
20		df-br 4002	. . . . . . . 8 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ ⟨𝐴, 𝑥⟩ ∈ (𝐹 ↾ 𝐵))
21		df-res 4636	. . . . . . . . 9 ⊢ (𝐹 ↾ 𝐵) = (𝐹 ∩ (𝐵 × V))
22	21	eleq2i 2244	. . . . . . . 8 ⊢ (⟨𝐴, 𝑥⟩ ∈ (𝐹 ↾ 𝐵) ↔ ⟨𝐴, 𝑥⟩ ∈ (𝐹 ∩ (𝐵 × V)))
23	20, 22	bitri 184	. . . . . . 7 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 ↔ ⟨𝐴, 𝑥⟩ ∈ (𝐹 ∩ (𝐵 × V)))
24		elin 3318	. . . . . . . 8 ⊢ (⟨𝐴, 𝑥⟩ ∈ (𝐹 ∩ (𝐵 × V)) ↔ (⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑥⟩ ∈ (𝐵 × V)))
25	24	simprbi 275	. . . . . . 7 ⊢ (⟨𝐴, 𝑥⟩ ∈ (𝐹 ∩ (𝐵 × V)) → ⟨𝐴, 𝑥⟩ ∈ (𝐵 × V))
26	23, 25	sylbi 121	. . . . . 6 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 → ⟨𝐴, 𝑥⟩ ∈ (𝐵 × V))
27		opelxp1 4658	. . . . . 6 ⊢ (⟨𝐴, 𝑥⟩ ∈ (𝐵 × V) → 𝐴 ∈ 𝐵)
28	26, 27	syl 14	. . . . 5 ⊢ (𝐴(𝐹 ↾ 𝐵)𝑥 → 𝐴 ∈ 𝐵)
29	28	exlimiv 1598	. . . 4 ⊢ (∃𝑥 𝐴(𝐹 ↾ 𝐵)𝑥 → 𝐴 ∈ 𝐵)
30	18, 19, 29	3syl 17	. . 3 ⊢ (𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴) → 𝐴 ∈ 𝐵)
31	30	con3i 632	. 2 ⊢ (¬ 𝐴 ∈ 𝐵 → ¬ 𝑧 ∈ ((𝐹 ↾ 𝐵)‘𝐴))
32	31	eq0rdv 3467	1 ⊢ (¬ 𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   = wceq 1353  ∃wex 1492  [wsb 1762  ∃!weu 2026   ∈ wcel 2148  {cab 2163  Vcvv 2737   ∩ cin 3128  ∅c0 3422  {csn 3592  ⟨cop 3595  ∪ cuni 3808   class class class wbr 4001   × cxp 4622   ↾ cres 4626  ℩cio 5173  ‘cfv 5213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4119  ax-pow 4172  ax-pr 4207

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-opab 4063  df-xp 4630  df-res 4636  df-iota 5175  df-fv 5221

This theorem is referenced by: (None)