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

Theorem fvn0ssdmfun 6465
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 6339. (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 6339 . . 3 ((𝐹𝑎) ≠ ∅ → (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
21ralimi 3054 . 2 (∀𝑎𝐷 (𝐹𝑎) ≠ ∅ → ∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})))
3 r19.26 3166 . . 3 (∀𝑎𝐷 (𝑎 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝑎})) ↔ (∀𝑎𝐷 𝑎 ∈ dom 𝐹 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})))
4 eleq1 2791 . . . . . 6 (𝑎 = 𝑝 → (𝑎 ∈ dom 𝐹𝑝 ∈ dom 𝐹))
54rspccv 3410 . . . . 5 (∀𝑎𝐷 𝑎 ∈ dom 𝐹 → (𝑝𝐷𝑝 ∈ dom 𝐹))
65ssrdv 3715 . . . 4 (∀𝑎𝐷 𝑎 ∈ dom 𝐹𝐷 ⊆ dom 𝐹)
7 funrel 6018 . . . . . . . 8 (Fun (𝐹 ↾ {𝑎}) → Rel (𝐹 ↾ {𝑎}))
87ralimi 3054 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
9 reliun 5347 . . . . . . 7 (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ∀𝑎𝐷 Rel (𝐹 ↾ {𝑎}))
108, 9sylibr 224 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Rel 𝑎𝐷 (𝐹 ↾ {𝑎}))
11 sneq 4295 . . . . . . . . . . . . . 14 (𝑎 = 𝑥 → {𝑎} = {𝑥})
1211reseq2d 5503 . . . . . . . . . . . . 13 (𝑎 = 𝑥 → (𝐹 ↾ {𝑎}) = (𝐹 ↾ {𝑥}))
1312funeqd 6023 . . . . . . . . . . . 12 (𝑎 = 𝑥 → (Fun (𝐹 ↾ {𝑎}) ↔ Fun (𝐹 ↾ {𝑥})))
1413rspcva 3411 . . . . . . . . . . 11 ((𝑥𝐷 ∧ ∀𝑎𝐷 Fun (𝐹 ↾ {𝑎})) → Fun (𝐹 ↾ {𝑥}))
15 dffun5 6014 . . . . . . . . . . . 12 (Fun (𝐹 ↾ {𝑥}) ↔ (Rel (𝐹 ↾ {𝑥}) ∧ ∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦)))
16 vex 3307 . . . . . . . . . . . . . . . . . . 19 𝑥 ∈ V
1716elsnres 5546 . . . . . . . . . . . . . . . . . 18 (⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) ↔ ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
1817imbi1i 338 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ (∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
1918albii 1860 . . . . . . . . . . . . . . . 16 (∀𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2019exbii 1887 . . . . . . . . . . . . . . 15 (∃𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
2120albii 1860 . . . . . . . . . . . . . 14 (∀𝑤𝑦𝑧(⟨𝑤, 𝑧⟩ ∈ (𝐹 ↾ {𝑥}) → 𝑧 = 𝑦) ↔ ∀𝑤𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦))
22 equcom 2064 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧𝑧 = 𝑎)
23 opeq12 4511 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑤 = 𝑥𝑧 = 𝑎) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2423ex 449 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 = 𝑥 → (𝑧 = 𝑎 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2522, 24syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = 𝑥 → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2625adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩))
2726impcom 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
28 opeq2 4510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 𝑎 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
2928equcoms 2066 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑎 = 𝑧 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑎⟩)
3029eleq1d 2788 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 = 𝑧 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 ↔ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3130biimpcd 239 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑧⟩ ∈ 𝐹 → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3231adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑎 = 𝑧 → ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3332impcom 445 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → ⟨𝑥, 𝑎⟩ ∈ 𝐹)
3427, 33jca 555 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 = 𝑧 ∧ (𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3534ex 449 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = 𝑧 → ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3635spimev 2368 . . . . . . . . . . . . . . . . . . 19 ((𝑤 = 𝑥 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹))
3736ex 449 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑥 → (⟨𝑥, 𝑧⟩ ∈ 𝐹 → ∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹)))
3837imim1d 82 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → ((∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
3938alimdv 1958 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → (∀𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4039eximdv 1959 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → (∃𝑦𝑧(∃𝑎(⟨𝑤, 𝑧⟩ = ⟨𝑥, 𝑎⟩ ∧ ⟨𝑥, 𝑎⟩ ∈ 𝐹) → 𝑧 = 𝑦) → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
4140spimvw 2046 . . . . . . . . . . . . . 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 1860 . . . . . . . . . . 11 (∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5150exbii 1887 . . . . . . . . . 10 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
52 19.21v 1981 . . . . . . . . . . 11 (∀𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5352exbii 1887 . . . . . . . . . 10 (∃𝑦𝑧(𝑥𝐷 → (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ ∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
54 19.37v 2039 . . . . . . . . . 10 (∃𝑦(𝑥𝐷 → ∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5551, 53, 543bitri 286 . . . . . . . . 9 (∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦) ↔ (𝑥𝐷 → ∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝐹𝑧 = 𝑦)))
5646, 55sylibr 224 . . . . . . . 8 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
5756alrimiv 1968 . . . . . . 7 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
58 resiun2 5528 . . . . . . . . . . . . . 14 (𝐹 𝑎𝐷 {𝑎}) = 𝑎𝐷 (𝐹 ↾ {𝑎})
5958eqcomi 2733 . . . . . . . . . . . . 13 𝑎𝐷 (𝐹 ↾ {𝑎}) = (𝐹 𝑎𝐷 {𝑎})
6059eleq2i 2795 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}))
61 iunid 4683 . . . . . . . . . . . . . 14 𝑎𝐷 {𝑎} = 𝐷
6261reseq2i 5500 . . . . . . . . . . . . 13 (𝐹 𝑎𝐷 {𝑎}) = (𝐹𝐷)
6362eleq2i 2795 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹 𝑎𝐷 {𝑎}) ↔ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷))
64 vex 3307 . . . . . . . . . . . . 13 𝑧 ∈ V
6564opelres 5511 . . . . . . . . . . . 12 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐷) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6660, 63, 653bitri 286 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷))
6766imbi1i 338 . . . . . . . . . 10 ((⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6867albii 1860 . . . . . . . . 9 (∀𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
6968exbii 1887 . . . . . . . 8 (∃𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∃𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7069albii 1860 . . . . . . 7 (∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦) ↔ ∀𝑥𝑦𝑧((⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥𝐷) → 𝑧 = 𝑦))
7157, 70sylibr 224 . . . . . 6 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦))
72 dffun5 6014 . . . . . 6 (Fun 𝑎𝐷 (𝐹 ↾ {𝑎}) ↔ (Rel 𝑎𝐷 (𝐹 ↾ {𝑎}) ∧ ∀𝑥𝑦𝑧(⟨𝑥, 𝑧⟩ ∈ 𝑎𝐷 (𝐹 ↾ {𝑎}) → 𝑧 = 𝑦)))
7310, 71, 72sylanbrc 701 . . . . 5 (∀𝑎𝐷 Fun (𝐹 ↾ {𝑎}) → Fun 𝑎𝐷 (𝐹 ↾ {𝑎}))
7461eqcomi 2733 . . . . . . . 8 𝐷 = 𝑎𝐷 {𝑎}
7574reseq2i 5500 . . . . . . 7 (𝐹𝐷) = (𝐹 𝑎𝐷 {𝑎})
7675funeqi 6022 . . . . . 6 (Fun (𝐹𝐷) ↔ Fun (𝐹 𝑎𝐷 {𝑎}))
7758funeqi 6022 . . . . . 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 1594   = wceq 1596  wex 1817  wcel 2103  wne 2896  wral 3014  wss 3680  c0 4023  {csn 4285  cop 4291   ciun 4628  dom cdm 5218  cres 5220  Rel wrel 5223  Fun wfun 5995  cfv 6001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-res 5230  df-iota 5964  df-fun 6003  df-fv 6009
This theorem is referenced by:  fveqressseq  6470  ovn0ssdmfun  42194
  Copyright terms: Public domain W3C validator