MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvn0ssdmfun Structured version   Visualization version   GIF version

Theorem fvn0ssdmfun 6572
Description: If a class' function values for certain arguments is not the empty set, the arguments are contained in the domain of the class, and the class restricted to the arguments is a function, analogous to fvfundmfvn0 6446. (Contributed by AV, 27-Jan-2020.)
Assertion
Ref Expression
fvn0ssdmfun (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
Distinct variable groups:   𝐷,𝑎   𝐹,𝑎

Proof of Theorem fvn0ssdmfun
Dummy variables 𝑝 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvfundmfvn0 6446 . . 3 ((𝐹𝑎) ≠ ∅ → (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
21ralimi 3140 . 2 (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → ∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
3 r19.26 3252 . . 3 (∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) ↔ (∀𝑎𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})))
4 eleq1w 2868 . . . . . 6 (𝑎 = 𝑝 → (𝑎 ∈ dom 𝐹𝑝 ∈ dom 𝐹))
54rspccv 3499 . . . . 5 (∀𝑎𝐷 𝑎 ∈ dom 𝐹 → (𝑝𝐷𝑝 ∈ dom 𝐹))
65ssrdv 3804 . . . 4 (∀𝑎𝐷 𝑎 ∈ dom 𝐹𝐷 ⊆ dom 𝐹)
7 funrel 6118 . . . . . . . 8 (Fun (𝐹 ↾ {𝑎}) → Rel (𝐹 ↾ {𝑎}))
87ralimi 3140 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
9 reliun 5441 . . . . . . 7 (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
108, 9sylibr 225 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Rel 𝑎𝐷 (𝐹 ↾ {𝑎}))
11 sneq 4380 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → {𝑎} = {𝑥})
1211reseq2d 5597 . . . . . . . . . . . . 13 (𝑎 = 𝑥 → (𝐹 ↾ {𝑎}) = (𝐹 ↾ {𝑥}))
1312funeqd 6123 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (Fun (𝐹 ↾ {𝑎}) ↔ Fun (𝐹 ↾ {𝑥})))
1413rspcva 3500 . . . . . . . . . . 11 ((𝑥𝐷 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → Fun (𝐹 ↾ {𝑥}))
15 dffun5 6114 . . . . . . . . . . . 12 (Fun (𝐹 ↾ {𝑥}) ↔ (Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)))
16 vex 3394 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
1716elsnres 5640 . . . . . . . . . . . . . . . . . 18 (⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) ↔ ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
1817imbi1i 340 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ (∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
1918albii 1904 . . . . . . . . . . . . . . . 16 (∀𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2019exbii 1933 . . . . . . . . . . . . . . 15 (∃𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2120albii 1904 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑤𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
22 equcom 2114 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧𝑧 = 𝑎)
23 opeq12 4597 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑤 = 𝑥𝑧 = 𝑎) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2423ex 399 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑥 → (𝑧 = 𝑎 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2522, 24syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2625adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2726impcom 396 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
28 opeq2 4596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑎 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2928equcoms 2116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
3029eleq1d 2870 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3130biimpcd 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑧⟩ ∈ 𝐹 → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3231adantl 469 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3332impcom 396 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑥, 𝑎⟩ ∈ 𝐹)
3427, 33jca 503 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3534ex 399 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑧 → ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3635spimev 2433 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3736ex 399 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3837imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → ((∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
3938alimdv 2007 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → (∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4039eximdv 2008 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → (∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4140spimvw 2096 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4221, 41sylbi 208 . . . . . . . . . . . . 13 (∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4342adantl 469 . . . . . . . . . . . 12 ((Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4415, 43sylbi 208 . . . . . . . . . . 11 (Fun (𝐹 ↾ {𝑥}) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4514, 44syl 17 . . . . . . . . . 10 ((𝑥𝐷 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4645expcom 400 . . . . . . . . 9 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
47 ancomst 452 . . . . . . . . . . . . 13 (((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ((𝑥𝐷 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑧 = 𝑦))
48 impexp 439 . . . . . . . . . . . . 13 (((𝑥𝐷 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4947, 48bitri 266 . . . . . . . . . . . 12 (((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5049albii 1904 . . . . . . . . . . 11 (∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5150exbii 1933 . . . . . . . . . 10 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
52 19.21v 2031 . . . . . . . . . . 11 (∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5352exbii 1933 . . . . . . . . . 10 (∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ ∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
54 19.37v 2089 . . . . . . . . . 10 (∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5551, 53, 543bitri 288 . . . . . . . . 9 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5646, 55sylibr 225 . . . . . . . 8 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
5756alrimiv 2018 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
58 resiun2 5621 . . . . . . . . . . . . . 14 (𝐹 𝑎𝐷 {𝑎}) = 𝑎𝐷 (𝐹 ↾ {𝑎})
5958eqcomi 2815 . . . . . . . . . . . . 13 𝑎𝐷 (𝐹 ↾ {𝑎}) = (𝐹 𝑎𝐷 {𝑎})
6059eleq2i 2877 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}))
61 iunid 4767 . . . . . . . . . . . . . 14 𝑎𝐷 {𝑎} = 𝐷
6261reseq2i 5594 . . . . . . . . . . . . 13 (𝐹 𝑎𝐷 {𝑎}) = (𝐹𝐷)
6362eleq2i 2877 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷))
64 vex 3394 . . . . . . . . . . . . 13 𝑧 ∈ V
6564opelres 5605 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6660, 63, 653bitri 288 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6766imbi1i 340 . . . . . . . . . 10 ((⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6867albii 1904 . . . . . . . . 9 (∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6968exbii 1933 . . . . . . . 8 (∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7069albii 1904 . . . . . . 7 (∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7157, 70sylibr 225 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦))
72 dffun5 6114 . . . . . 6 (Fun 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ∧ ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦)))
7310, 71, 72sylanbrc 574 . . . . 5 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7461eqcomi 2815 . . . . . . . 8 𝐷 = 𝑎𝐷 {𝑎}
7574reseq2i 5594 . . . . . . 7 (𝐹𝐷) = (𝐹 𝑎𝐷 {𝑎})
7675funeqi 6122 . . . . . 6 (Fun (𝐹𝐷) ↔ Fun (𝐹 𝑎𝐷 {𝑎}))
7758funeqi 6122 . . . . . 6 (Fun (𝐹 𝑎𝐷 {𝑎}) ↔ Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7876, 77bitri 266 . . . . 5 (Fun (𝐹𝐷) ↔ Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7973, 78sylibr 225 . . . 4 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Fun (𝐹𝐷))
806, 79anim12i 602 . . 3 ((∀𝑎𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
813, 80sylbi 208 . 2 (∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
822, 81syl 17 1 (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2156  wne 2978  wral 3096  wss 3769  c0 4116  {csn 4370  cop 4376   ciun 4712  dom cdm 5311  cres 5313  Rel wrel 5316  Fun wfun 6095  cfv 6101
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-res 5323  df-iota 6064  df-fun 6103  df-fv 6109
This theorem is referenced by:  fveqressseq  6577  ovn0ssdmfun  42335
  Copyright terms: Public domain W3C validator