NFE Home New Foundations Explorer This is the Unicode version.
Change to GIF version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3wff ¬ φ
wi 4wff (φψ)
ax-1 5(φ → (ψφ))
ax-2 6((φ → (ψχ)) → ((φψ) → (φχ)))
ax-3 7((¬ φ → ¬ ψ) → (ψφ))
ax-mp 8φ    &   (φψ)       ψ
wb 176wff (φψ)
df-bi 177 ¬ (((φψ) → ¬ ((φψ) → ¬ (ψφ))) → ¬ (¬ ((φψ) → ¬ (ψφ)) → (φψ)))
wo 357wff (φ ψ)
wa 358wff (φ ψ)
df-or 359((φ ψ) ↔ (¬ φψ))
df-an 360((φ ψ) ↔ ¬ (φ → ¬ ψ))
w3o 933wff (φ ψ χ)
w3a 934wff (φ ψ χ)
df-3or 935((φ ψ χ) ↔ ((φ ψ) χ))
df-3an 936((φ ψ χ) ↔ ((φ ψ) χ))
wnan 1287wff (φ ψ)
df-nan 1288((φ ψ) ↔ ¬ (φ ψ))
wxo 1304wff (φψ)
df-xor 1305((φψ) ↔ ¬ (φψ))
wtru 1316wff
wfal 1317wff
df-tru 1319( ⊤ ↔ (φφ))
df-fal 1320( ⊥ ↔ ¬ ⊤ )
whad 1378wff hadd(φ, ψ, χ)
wcad 1379wff cadd(φ, ψ, χ)
df-had 1380(hadd(φ, ψ, χ) ↔ ((φψ) ⊻ χ))
df-cad 1381(cadd(φ, ψ, χ) ↔ ((φ ψ) (χ (φψ))))
ax-meredith 1406(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
wal 1540wff xφ
wex 1541wff xφ
df-ex 1542(xφ ↔ ¬ x ¬ φ)
wnf 1544wff xφ
df-nf 1545(Ⅎxφx(φxφ))
ax-gen 1546φ       xφ
ax-5 1557(x(φψ) → (xφxψ))
ax-17 1616(φxφ)
cv 1641class x
wceq 1642wff A = B
wsb 1648wff [y / x]φ
df-sb 1649([y / x]φ ↔ ((x = yφ) x(x = y φ)))
ax-9 1654 ¬ x ¬ x = y
ax-8 1675(x = y → (x = zy = z))
wcel 1710wff A B
ax-13 1712(x = y → (x zy z))
ax-14 1714(x = y → (z xz y))
ax-6 1729xφx ¬ xφ)
ax-7 1734(xyφyxφ)
ax-11 1746(x = y → (yφx(x = yφ)))
ax-12 1925x = y → (y = zx y = z))
ax-4 2135(xφφ)
ax-5o 2136(x(xφψ) → (xφxψ))
ax-6o 2137x ¬ xφφ)
ax-9o 2138(x(x = yxφ) → φ)
ax-10o 2139(x x = y → (xφyφ))
ax-10 2140(x x = yy y = x)
ax-11o 2141x x = y → (x = y → (φx(x = yφ))))
ax-12o 2142z z = x → (¬ z z = y → (x = yz x = y)))
ax-15 2143z z = x → (¬ z z = y → (x yz x y)))
ax-16 2144(x x = y → (φxφ))
weu 2204wff ∃!xφ
wmo 2205wff ∃*xφ
df-eu 2208(∃!xφyx(φx = y))
df-mo 2209(∃*xφ ↔ (xφ∃!xφ))
ax-7d 2295(xyφyxφ)
ax-8d 2296(x = y → (x = zy = z))
ax-9d1 2297 ¬ x ¬ x = x
ax-9d2 2298 ¬ x ¬ x = y
ax-10d 2299(x x = yy y = x)
ax-11d 2300(x = y → (yφx(x = yφ)))
ax-ext 2334(z(z xz y) → x = y)
cab 2339class {x φ}
df-clab 2340(x {y φ} ↔ [x / y]φ)
df-cleq 2346(x(x yx z) → y = z)       (A = Bx(x Ax B))
df-clel 2349(A Bx(x = A x B))
wnfc 2476wff xA
df-nfc 2478(xAyx y A)
wne 2516wff AB
wnel 2517wff A B
df-ne 2518(AB ↔ ¬ A = B)
df-nel 2519(A B ↔ ¬ A B)
wral 2614wff x A φ
wrex 2615wff x A φ
wreu 2616wff ∃!x A φ
wrmo 2617wff ∃*x A φ
crab 2618class {x A φ}
df-ral 2619(x A φx(x Aφ))
df-rex 2620(x A φx(x A φ))
df-reu 2621(∃!x A φ∃!x(x A φ))
df-rmo 2622(∃*x A φ∃*x(x A φ))
df-rab 2623{x A φ} = {x (x A φ)}
cvv 2859class V
df-v 2861V = {x x = x}
wsbc 3046wff A / xφ
df-sbc 3047([̣A / xφA {x φ})
csb 3136class [A / x]B
df-csb 3137[A / x]B = {y A / xy B}
cnin 3204class (AB)
ccompl 3205class A
cdif 3206class (A B)
cun 3207class (AB)
cin 3208class (AB)
csymdif 3209class (AB)
df-nin 3211(AB) = {x (x A x B)}
df-compl 3212A = (AA)
df-in 3213(AB) = ∼ (AB)
df-un 3214(AB) = ( ∼ A ⩃ ∼ B)
df-dif 3215(A B) = (A ∩ ∼ B)
df-symdif 3216(AB) = ((A B) ∪ (B A))
wss 3257wff A B
wpss 3258wff AB
df-ss 3259(A B ↔ (AB) = A)
df-pss 3261(AB ↔ (A B AB))
c0 3550class
df-nul 3551 = (V V)
cif 3662class if(φ, A, B)
df-if 3663 if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}
cpw 3722class A
df-pw 3724A = {x x A}
csn 3737class {A}
cpr 3738class {A, B}
ctp 3739class {A, B, C}
df-sn 3741{A} = {x x = A}
df-pr 3742{A, B} = ({A} ∪ {B})
df-tp 3743{A, B, C} = ({A, B} ∪ {C})
cuni 3891class A
df-uni 3892A = {x y(x y y A)}
cint 3926class A
df-int 3927A = {x y(y Ax y)}
ciun 3969class x A B
ciin 3970class x A B
df-iun 3971x A B = {y x A y B}
df-iin 3972x A B = {y x A y B}
copk 4057class A, B
df-opk 4058A, B⟫ = {{A}, {A, B}}
ax-nin 4078zw(w z ↔ (w x w y))
ax-xp 4079yz(z ywt(z = ⟪w, t t x))
ax-cnv 4080yzw(⟪z, w y ↔ ⟪w, z x)
ax-1c 4081xy(y xzw(w yw = z))
ax-sset 4082xyz(⟪y, z xw(w yw z))
ax-si 4083yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
ax-ins2 4084yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x)
ax-ins3 4085yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, w x)
ax-typlower 4086yz(z yww, {z}⟫ x)
ax-sn 4087yz(z yz = x)
cuni1 4133class 1A
c1c 4134class 1c
cpw1 4135class 1A
df-1c 41361c = {x y x = {y}}
df-pw1 41371A = (A ∩ 1c)
df-uni1 41381A = (A ∩ 1c)
cxpk 4174class (A ×k B)
ccnvk 4175class kA
cins2k 4176class Ins2k A
cins3k 4177class Ins3k A
cp6 4178class P6 A
cimak 4179class (Ak B)
ccomk 4180class (A k B)
csik 4181class SIk A
cimagek 4182class ImagekA
cssetk 4183class Sk
cidk 4184class Ik
df-xpk 4185(A ×k B) = {x yz(x = ⟪y, z (y A z B))}
df-cnvk 4186kA = {x yz(x = ⟪y, zz, y A)}
df-ins2k 4187 Ins2k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, v A))}
df-ins3k 4188 Ins3k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, u A))}
df-imak 4189(Ak B) = {x y By, x A}
df-cok 4190(A k B) = (( Ins2k AIns3k kB) “k V)
df-p6 4191 P6 A = {x (V ×k {{x}}) A}
df-sik 4192 SIk A = {x yz(x = ⟪y, z tu(y = {t} z = {u} t, u A))}
df-ssetk 4193 Sk = {x yz(x = ⟪y, z y z)}
df-imagek 4194ImagekA = ((V ×k V) (( Ins2k SkIns3k ( Sk k k SIk A)) “k 111c))
df-idk 4195 Ik = {x yz(x = ⟪y, z y = z)}
cio 4337class (℩xφ)
df-iota 4339(℩xφ) = {y {x φ} = {y}}
cnnc 4373class Nn
c0c 4374class 0c
cplc 4375class (A +c B)
cfin 4376class Fin
df-0c 43770c = {}
df-addc 4378(A +c B) = {x y A z B ((yz) = x = (yz))}
df-nnc 4379 Nn = {b (0c b y b (y +c 1c) b)}
df-fin 4380 Fin = Nn
clefin 4432class fin
cltfin 4433class <fin
cncfin 4434class Ncfin A
ctfin 4435class Tfin A
cevenfin 4436class Evenfin
coddfin 4437class Oddfin
wsfin 4438wff Sfin (A, B)
cspfin 4439class Spfin
df-lefin 4440fin = {x yz(x = ⟪y, z w Nn z = (y +c w))}
df-ltfin 4441 <fin = {x mn(x = ⟪m, n (m p Nn n = ((m +c p) +c 1c)))}
df-ncfin 4442 Ncfin A = (℩x(x Nn A x))
df-tfin 4443 Tfin M = if(M = , , (℩n(n Nn a M 1a n)))
df-evenfin 4444 Evenfin = {x (n Nn x = (n +c n) x)}
df-oddfin 4445 Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
df-sfin 4446( Sfin (M, N) ↔ (M Nn N Nn a(1a M a N)))
df-spfin 4447 Spfin = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
cop 4562class A, B
cphi 4563class Phi A
cproj1 4564class Proj1 A
cproj2 4565class Proj2 A
df-phi 4566 Phi A = {y x A y = if(x Nn , (x +c 1c), x)}
df-op 4567A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
df-proj1 4568 Proj1 A = {x Phi x A}
df-proj2 4569 Proj2 A = {x ( Phi x ∪ {0c}) A}
copab 4615class {x, y φ}
df-opab 4616{x, y φ} = {z xy(z = x, y φ)}
wbr 4632wff ARB
df-br 4633(ARBA, B R)
c1st 4710class 1st
cswap 4711class Swap
csset 4712class S
csi 4713class SI A
ccom 4714class (A B)
cima 4715class (AB)
df-1st 47161st = {x, y z x = y, z}
df-swap 4717 Swap = {x, y zw(x = z, w y = w, z)}
df-sset 4718 S = {x, y x y}
df-co 4719(A B) = {x, y z(xBz zAy)}
df-ima 4720(AB) = {x y B yAx}
df-si 4721 SI A = {x, y zw(x = {z} y = {w} zAw)}
cep 4755class E
cid 4756class I
df-eprel 4757 E = {x, y x y}
df-id 4760 I = {x, y x = y}
cxp 4763class (A × B)
ccnv 4764class A
cdm 4765class dom A
crn 4766class ran A
cres 4767class (A B)
wrel 4768wff Rel A
wfun 4769wff Fun A
wfn 4770wff A Fn B
wf 4771wff F:A–→B
wf1 4772wff F:A1-1B
wfo 4773wff F:AontoB
wf1o 4774wff F:A1-1-ontoB
cfv 4775class (FA)
wiso 4776wff H Isom R, S (A, B)
c2nd 4777class 2nd
df-xp 4778(A × B) = {x, y (x A y B)}
df-rel 4779(Rel AA (V × V))
df-cnv 4780A = {x, y yAx}
df-rn 4781ran A = (A “ V)
df-dm 4782dom A = ran A
df-res 4783(A B) = (A ∩ (B × V))
df-fun 4784(Fun A ↔ (Rel A (A A) I ))
df-fn 4785(A Fn B ↔ (Fun A dom A = B))
df-f 4786(F:A–→B ↔ (F Fn A ran F B))
df-f1 4787(F:A1-1B ↔ (F:A–→B Fun F))
df-fo 4788(F:AontoB ↔ (F Fn A ran F = B))
df-f1o 4789(F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))
df-fv 4790(FA) = (℩xAFx)
df-iso 4791(H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))
df-2nd 47922nd = {x, y z x = z, y}
co 5565class (AFB)
df-ov 5566(AFB) = (FA, B)
coprab 5567class {x, y, z φ}
df-oprab 5568{x, y, z φ} = {w xyz(w = x, y, z φ)}
cmpt 5692class (x A B)
df-mpt 5693(x A B) = {x, y (x A y = B)}
cmpt2 5694class (x A, y B C)
df-mpt2 5695(x A, y B C) = {x, y, z ((x A y B) z = C)}
ctxp 5772class (AB)
df-txp 5773(AB) = ((1st A) ∩ (2nd B))
cpprod 5774class PProd (A, B)
df-pprod 5775 PProd (A, B) = ((A 1st ) ⊗ (B 2nd ))
cfix 5776class Fix A
df-fix 5777 Fix A = ran (A ∩ I )
ccup 5778class Cup
df-cup 5779 Cup = (x V, y V (xy))
cdisj 5780class Disj
df-disj 5781 Disj = {x, y (xy) = }
caddcfn 5782class AddC
df-addcfn 5783 AddC = (x V, y V (x +c y))
cins2 5784class Ins2 A
df-ins2 5785 Ins2 A = (V ⊗ A)
cins3 5786class Ins3 A
df-ins3 5787 Ins3 A = (A ⊗ V)
cimage 5788class ImageA
df-image 5789ImageA = ((V × V) (( Ins2 S Ins3 ( S SI A)) “ 1c))
cins4 5790class Ins4 A
df-ins4 5791 Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)
csi3 5792class SI3 A
df-si3 5793 SI3 A = (( SI 1st ⊗ ( SI (1st 2nd ) ⊗ SI (2nd 2nd ))) “ 1A)
cfuns 5794class Funs
df-funs 5795 Funs = {f Fun f}
cfns 5796class Fns
df-fns 5797 Fns = {f, a f Fn a}
ccross 5798class Cross
df-cross 5799 Cross = (x V, y V (x × y))
cpw1fn 5800class Pw1Fn
df-pw1fn 5801 Pw1Fn = (x 1c 1x)
cfullfun 5802class FullFun F
df-fullfun 5803 FullFun F = ((( I F) ( ∼ I F)) ∪ ( ∼ dom (( I F) ( ∼ I F)) × {}))
cdomfn 5804class Dom
df-domfn 5805 Dom = (x V dom x)
cranfn 5806class Ran
df-ranfn 5807 Ran = (x V ran x)
cclos1 5909class Clos1 (A, R)
df-clos1 5910 Clos1 (S, R) = {a (S a (Ra) a)}
ctrans 5925class Trans
cref 5926class Ref
cantisym 5927class Antisym
cpartial 5928class Po
cconnex 5929class Connex
cstrict 5930class Or
cfound 5931class Fr
cwe 5932class We
cext 5933class Ext
csym 5934class Sym
cer 5935class Er
df-trans 5936 Trans = {r, a x a y a z a ((xry yrz) → xrz)}
df-ref 5937 Ref = {r, a x a xrx}
df-antisym 5938 Antisym = {r, a x a y a ((xry yrx) → x = y)}
df-partial 5939 Po = (( RefTrans ) ∩ Antisym )
df-connex 5940 Connex = {r, a x a y a (xry yrx)}
df-strict 5941 Or = ( PoConnex )
df-found 5942 Fr = {r, a x((x a x) → z x y x (yrzy = z))}
df-we 5943 We = ( OrFr )
df-ext 5944 Ext = {r, a x a y a (z a (zrxzry) → x = y)}
df-sym 5945 Sym = {r, a x a y a (xryyrx)}
df-er 5946 Er = ( SymTrans )
cec 5982class [A]R
cqs 5983class (A / R)
df-ec 5984[A]R = (R “ {A})
df-qs 5988(A / R) = {y x A y = [x]R}
cmap 6036class m
cpm 6037class pm
df-map 6038m = (x V, y V {f f:y–→x})
df-pm 6039pm = (x V, y V {f (y × x) Fun f})
cen 6065class
df-en 6066 ≈ = {x, y f f:x1-1-ontoy}
cncs 6125class NC
clec 6126class c
cltc 6127class <c
cnc 6128class Nc A
cmuc 6129class ·c
ctc 6130class Tc A
c2c 6131class 2c
c3c 6132class 3c
cce 6133class c
ctcfn 6134class TcFn
df-ncs 6135 NC = (V / ≈ )
df-lec 6136c = {a, b x a y b x y}
df-ltc 6137 <c = ( ≤c I )
df-nc 6138 Nc A = [A] ≈
df-muc 6139 ·c = (m NC , n NC {a b m g n a ≈ (b × g)})
df-tc 6140 Tc A = (℩b(b NC x A b = Nc 1x))
df-2c 61412c = Nc {, V}
df-3c 61423c = Nc {, V, (V {})}
df-ce 6143c = (n NC , m NC {g ab(1a n 1b m g ≈ (am b))})
df-tcfn 6144TcFn = (x 1c Tc x)
cspac 6309class Spac
df-spac 6310 Spac = (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
cfrec 6345class FRec (F, I)
df-frec 6346 FRec (F, I) = Clos1 ({0c, I}, PProd ((x V (x +c 1c)), F))
  Copyright terms: Public domain W3C validator