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

Theorem fvn0ssdmfun 6513
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 6387. (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 6387 . . 3 ((𝐹𝑎) ≠ ∅ → (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
21ralimi 3090 . 2 (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → ∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
3 r19.26 3202 . . 3 (∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) ↔ (∀𝑎𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})))
4 eleq1w 2822 . . . . . 6 (𝑎 = 𝑝 → (𝑎 ∈ dom 𝐹𝑝 ∈ dom 𝐹))
54rspccv 3446 . . . . 5 (∀𝑎𝐷 𝑎 ∈ dom 𝐹 → (𝑝𝐷𝑝 ∈ dom 𝐹))
65ssrdv 3750 . . . 4 (∀𝑎𝐷 𝑎 ∈ dom 𝐹𝐷 ⊆ dom 𝐹)
7 funrel 6066 . . . . . . . 8 (Fun (𝐹 ↾ {𝑎}) → Rel (𝐹 ↾ {𝑎}))
87ralimi 3090 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
9 reliun 5395 . . . . . . 7 (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
108, 9sylibr 224 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Rel 𝑎𝐷 (𝐹 ↾ {𝑎}))
11 sneq 4331 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → {𝑎} = {𝑥})
1211reseq2d 5551 . . . . . . . . . . . . 13 (𝑎 = 𝑥 → (𝐹 ↾ {𝑎}) = (𝐹 ↾ {𝑥}))
1312funeqd 6071 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (Fun (𝐹 ↾ {𝑎}) ↔ Fun (𝐹 ↾ {𝑥})))
1413rspcva 3447 . . . . . . . . . . 11 ((𝑥𝐷 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → Fun (𝐹 ↾ {𝑥}))
15 dffun5 6062 . . . . . . . . . . . 12 (Fun (𝐹 ↾ {𝑥}) ↔ (Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)))
16 vex 3343 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
1716elsnres 5594 . . . . . . . . . . . . . . . . . 18 (⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) ↔ ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
1817imbi1i 338 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ (∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
1918albii 1896 . . . . . . . . . . . . . . . 16 (∀𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2019exbii 1923 . . . . . . . . . . . . . . 15 (∃𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2120albii 1896 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑤𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
22 equcom 2100 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧𝑧 = 𝑎)
23 opeq12 4555 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑤 = 𝑥𝑧 = 𝑎) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2423ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑥 → (𝑧 = 𝑎 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2522, 24syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2625adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2726impcom 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
28 opeq2 4554 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑎 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2928equcoms 2102 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
3029eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3130biimpcd 239 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑧⟩ ∈ 𝐹 → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3231adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3332impcom 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑥, 𝑎⟩ ∈ 𝐹)
3427, 33jca 555 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3534ex 449 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑧 → ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3635spimev 2404 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3736ex 449 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3837imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → ((∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
3938alimdv 1994 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → (∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4039eximdv 1995 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → (∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4140spimvw 2082 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4221, 41sylbi 207 . . . . . . . . . . . . 13 (∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4342adantl 473 . . . . . . . . . . . 12 ((Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4415, 43sylbi 207 . . . . . . . . . . 11 (Fun (𝐹 ↾ {𝑥}) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4514, 44syl 17 . . . . . . . . . 10 ((𝑥𝐷 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦))
4645expcom 450 . . . . . . . . 9 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
47 ancomst 467 . . . . . . . . . . . . 13 (((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ((𝑥𝐷 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑧 = 𝑦))
48 impexp 461 . . . . . . . . . . . . 13 (((𝑥𝐷 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4947, 48bitri 264 . . . . . . . . . . . 12 (((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5049albii 1896 . . . . . . . . . . 11 (∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5150exbii 1923 . . . . . . . . . 10 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
52 19.21v 2017 . . . . . . . . . . 11 (∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5352exbii 1923 . . . . . . . . . 10 (∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ ∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
54 19.37v 2075 . . . . . . . . . 10 (∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5551, 53, 543bitri 286 . . . . . . . . 9 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5646, 55sylibr 224 . . . . . . . 8 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
5756alrimiv 2004 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
58 resiun2 5576 . . . . . . . . . . . . . 14 (𝐹 𝑎𝐷 {𝑎}) = 𝑎𝐷 (𝐹 ↾ {𝑎})
5958eqcomi 2769 . . . . . . . . . . . . 13 𝑎𝐷 (𝐹 ↾ {𝑎}) = (𝐹 𝑎𝐷 {𝑎})
6059eleq2i 2831 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}))
61 iunid 4727 . . . . . . . . . . . . . 14 𝑎𝐷 {𝑎} = 𝐷
6261reseq2i 5548 . . . . . . . . . . . . 13 (𝐹 𝑎𝐷 {𝑎}) = (𝐹𝐷)
6362eleq2i 2831 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷))
64 vex 3343 . . . . . . . . . . . . 13 𝑧 ∈ V
6564opelres 5559 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6660, 63, 653bitri 286 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6766imbi1i 338 . . . . . . . . . 10 ((⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6867albii 1896 . . . . . . . . 9 (∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6968exbii 1923 . . . . . . . 8 (∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7069albii 1896 . . . . . . 7 (∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7157, 70sylibr 224 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦))
72 dffun5 6062 . . . . . 6 (Fun 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ∧ ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦)))
7310, 71, 72sylanbrc 701 . . . . 5 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7461eqcomi 2769 . . . . . . . 8 𝐷 = 𝑎𝐷 {𝑎}
7574reseq2i 5548 . . . . . . 7 (𝐹𝐷) = (𝐹 𝑎𝐷 {𝑎})
7675funeqi 6070 . . . . . 6 (Fun (𝐹𝐷) ↔ Fun (𝐹 𝑎𝐷 {𝑎}))
7758funeqi 6070 . . . . . 6 (Fun (𝐹 𝑎𝐷 {𝑎}) ↔ Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7876, 77bitri 264 . . . . 5 (Fun (𝐹𝐷) ↔ Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7973, 78sylibr 224 . . . 4 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Fun (𝐹𝐷))
806, 79anim12i 591 . . 3 ((∀𝑎𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
813, 80sylbi 207 . 2 (∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
822, 81syl 17 1 (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → (𝐷 ⊆ dom 𝐹 ∧ Fun (𝐹𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1630   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wss 3715  c0 4058  {csn 4321  cop 4327   ciun 4672  dom cdm 5266  cres 5268  Rel wrel 5271  Fun wfun 6043  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-res 5278  df-iota 6012  df-fun 6051  df-fv 6057
This theorem is referenced by:  fveqressseq  6518  ovn0ssdmfun  42277
  Copyright terms: Public domain W3C validator