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
17675 sscfn1
17799 sscfn2
17800 ssclem
17801 isssc
17802 rescval2
17810 issubc2
17821 cofuval
17867 resfval2
17878 resf1st
17879 psssdm2
18572 tsrss
18580 decpmatval
22697 pmatcollpw3lem
22715 ustssco
24149 ustbas2
24160 psmetdmdm
24241 xmetdmdm
24271 setsmstopn
24416 tmsval
24419 tngtopn
24597 caufval
25233 grporndm
30376 dfhnorm2
30988 hhshsslem1
31133 metideq
33564 filnetlem4
35935 poimirlem3
37166 ssbnd
37331 bnd2lem
37334 ismtyval
37343 ismndo2
37417 exidreslem
37420 divrngcl
37500 isdrngo2
37501 rtrclex
43112 fnxpdmdm
47334 |