Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1533 ∅c0 4323
× cxp 5675 dom cdm 5677 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5299 ax-nul 5306 ax-pr 5428 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rab 3420 df-v 3465 df-dif 3948 df-un 3950 df-ss 3962 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5149 df-opab 5211 df-xp 5683 df-dm 5687 |
This theorem is referenced by: dmxpin
5932 xpid11
5933 sofld
6191 xpider
8805 hartogslem1
9565 unxpwdom2
9611 infxpenlem
10036 fpwwe2lem12
10665 fpwwe2
10666 canth4
10670 dmrecnq
10991 homfeqbas
17676 sscfn1
17800 sscfn2
17801 ssclem
17802 isssc
17803 rescval2
17811 issubc2
17822 cofuval
17868 resfval2
17879 resf1st
17880 psssdm2
18573 tsrss
18581 decpmatval
22698 pmatcollpw3lem
22716 ustssco
24150 ustbas2
24161 psmetdmdm
24242 xmetdmdm
24272 setsmstopn
24417 tmsval
24420 tngtopn
24598 caufval
25234 grporndm
30377 dfhnorm2
30989 hhshsslem1
31134 metideq
33581 filnetlem4
35952 poimirlem3
37183 ssbnd
37348 bnd2lem
37351 ismtyval
37360 ismndo2
37434 exidreslem
37437 divrngcl
37517 isdrngo2
37518 rtrclex
43129 fnxpdmdm
47350 |