Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
class class class wbr 5147 ≈ cen 8938
≼ cdom 8939 ≺
csdm 8940 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-dif 3950 df-br 5148 df-sdom 8944 |
This theorem is referenced by: bren2
8981 domdifsn
9056 sucdom2OLD
9084 sdomnsym
9100 domnsym
9101 sdomirr
9116 domnsymfi
9205 sucdom2
9208 php5
9216 phpeqd
9217 phpeqdOLD
9227 1sdom2dom
9249 pssinf
9258 f1finf1o
9273 f1finf1oOLD
9274 isfinite2
9303 cardom
9983 pm54.43
9998 pr2neOLD
10002 alephdom
10078 cdainflem
10184 ackbij1b
10236 isfin4p1
10312 fin23lem25
10321 fin67
10392 axcclem
10454 canthp1lem2
10650 gchinf
10654 pwfseqlem4
10659 tskssel
10754 1nprm
16620 en2top
22708 domalom
36588 pibt2
36601 rp-isfinite6
42571 ensucne0OLD
42583 iscard5
42589 omiscard
42596 |