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 F/_xA
df-nfc 2478(F/_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 / x].y 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 A B
df-ss 3259(A B ↔ (AB) = A)
df-pss 3261(A B ↔ (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 SSetk
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 SSetk = {x yz(x = ⟪y, z y z)}
df-imagek 4194ImagekA = ((V ×k V) (( Ins2k SSetkIns3k ( SSetk 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 4431class fin
cltfin 4432class <fin
cncfin 4433class Ncfin A
ctfin 4434class Tfin A
cevenfin 4435class Evenfin
coddfin 4436class Oddfin
wsfin 4437wff Sfin (A, B)
cspfin 4438class Spfin
df-lefin 4439fin = {x yz(x = ⟪y, z w Nn z = (y +c w))}
df-ltfin 4440 <fin = {x mn(x = ⟪m, n (m p Nn n = ((m +c p) +c 1c)))}
df-ncfin 4441 Ncfin A = (℩x(x Nn A x))
df-tfin 4442 Tfin M = if(M = , , (℩n(n Nn a M 1a n)))
df-evenfin 4443 Evenfin = {x (n Nn x = (n +c n) x)}
df-oddfin 4444 Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
df-sfin 4445( Sfin (M, N) ↔ (M Nn N Nn a(1a M a N)))
df-spfin 4446 Spfin = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
cop 4561class A, B
cphi 4562class Phi A
cproj1 4563class Proj1 A
cproj2 4564class Proj2 A
df-phi 4565 Phi A = {y x A y = if(x Nn , (x +c 1c), x)}
df-op 4566A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
df-proj1 4567 Proj1 A = {x Phi x A}
df-proj2 4568 Proj2 A = {x ( Phi x ∪ {0c}) A}
copab 4614class {x, y φ}
df-opab 4615{x, y φ} = {z xy(z = x, y φ)}
wbr 4631wff ARB
df-br 4632(ARBA, B R)
c1st 4709class 1st
cswap 4710class Swap
csset 4711class SSet
csi 4712class SI A
ccom 4713class (A B)
cima 4714class (AB)
df-1st 47151st = {x, y z x = y, z}
df-swap 4716 Swap = {x, y zw(x = z, w y = w, z)}
df-sset 4717 SSet = {x, y x y}
df-co 4718(A B) = {x, y z(xBz zAy)}
df-ima 4719(AB) = {x y B yAx}
df-si 4720 SI A = {x, y zw(x = {z} y = {w} zAw)}
cep 4754class E
cid 4755class I
df-eprel 4756 E = {x, y x y}
df-id 4759 I = {x, y x = y}
cxp 4762class (A × B)
ccnv 4763class A
cdm 4764class dom A
crn 4765class ran A
cres 4766class (A B)
wrel 4767wff Rel A
wfun 4768wff Fun A
wfn 4769wff A Fn B
wf 4770wff F:A–→B
wf1 4771wff F:A1-1B
wfo 4772wff F:AontoB
wf1o 4773wff F:A1-1-ontoB
cfv 4774class (FA)
wiso 4775wff H Isom R, S (A, B)
c2nd 4776class 2nd
df-xp 4777(A × B) = {x, y (x A y B)}
df-rel 4778(Rel AA (V × V))
df-cnv 4779A = {x, y yAx}
df-rn 4780ran A = (A “ V)
df-dm 4781dom A = ran A
df-res 4782(A B) = (A ∩ (B × V))
df-fun 4783(Fun A ↔ (Rel A (A A) I ))
df-fn 4784(A Fn B ↔ (Fun A dom A = B))
df-f 4785(F:A–→B ↔ (F Fn A ran F B))
df-f1 4786(F:A1-1B ↔ (F:A–→B Fun F))
df-fo 4787(F:AontoB ↔ (F Fn A ran F = B))
df-f1o 4788(F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))
df-fv 4789(FA) = (℩xAFx)
df-iso 4790(H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))
df-2nd 47912nd = {x, y z x = z, y}
co 5564class (AFB)
coprab 5565class {x, y, z φ}
df-ov 5566(AFB) = (FA, B)
df-oprab 5567{x, y, z φ} = {w xyz(w = x, y, z φ)}
cmpt 5691class (x A B)
cmpt2 5692class (x A, y B C)
df-mpt 5693(x A B) = {x, y (x A y = B)}
df-mpt2 5694(x A, y B C) = {x, y, z ((x A y B) z = C)}
ctxp 5771class (AB)
cpprod 5772class PProd (A, B)
cfix 5773class Fix A
cimage 5774class ImageA
ccup 5775class Cup
cdisj 5776class Disj
caddcfn 5777class AddC
cins2 5778class Ins2 A
cins3 5779class Ins3 A
cins4 5780class Ins4 A
csi3 5781class SI3 A
cfuns 5782class Funs
cfns 5783class Fns
ccross 5784class Cross
cpw1fn 5785class Pw1Fn
cfullfun 5786class FullFun F
df-txp 5787(AB) = ((1st A) ∩ (2nd B))
df-pprod 5788 PProd (A, B) = ((A 1st ) ⊗ (B 2nd ))
df-fix 5789 Fix A = ran (A ∩ I )
df-cup 5790 Cup = (x V, y V (xy))
df-disj 5791 Disj = {x, y (xy) = }
df-addcfn 5792 AddC = (x V, y V (x +c y))
df-ins2 5793 Ins2 A = (V ⊗ A)
df-ins3 5794 Ins3 A = (A ⊗ V)
df-image 5795ImageA = ((V × V) (( Ins2 SSet Ins3 ( SSet SI A)) “ 1c))
df-ins4 5796 Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)
df-si3 5797 SI3 A = (( SI 1st ⊗ ( SI (1st 2nd ) ⊗ SI (2nd 2nd ))) “ 1A)
df-funs 5798 Funs = {f Fun f}
df-fns 5799 Fns = {f, a f Fn a}
df-cross 5800 Cross = (x V, y V (x × y))
df-pw1fn 5801 Pw1Fn = (x 1c 1x)
df-fullfun 5802 FullFun F = ((( I F) ( ∼ I F)) ∪ ( ∼ dom (( I F) ( ∼ I F)) × {}))
cclos1 5894class Clos1 (A, R)
df-clos1 5895 Clos1 (S, R) = {a (S a (Ra) a)}
ctrans 5908class Trans
cref 5909class Ref
cantisym 5910class Antisym
cpartial 5911class Po
cconnex 5912class Connex
cstrict 5913class Or
cfound 5914class Fr
cwe 5915class We
cext 5916class Ext
csym 5917class Sym
cer 5918class Er
df-trans 5919 Trans = {r, a x a y a z a ((xry yrz) → xrz)}
df-ref 5920 Ref = {r, a x a xrx}
df-antisym 5921 Antisym = {r, a x a y a ((xry yrx) → x = y)}
df-partial 5922 Po = (( RefTrans ) ∩ Antisym )
df-connex 5923 Connex = {r, a x a y a (xry yrx)}
df-strict 5924 Or = ( PoConnex )
df-found 5925 Fr = {r, a x((x a x) → z x y x (yrzy = z))}
df-we 5926 We = ( OrFr )
df-ext 5927 Ext = {r, a x a y a (z a (zrxzry) → x = y)}
df-sym 5928 Sym = {r, a x a y a (xryyrx)}
df-er 5929 Er = ( SymTrans )
cec 5965class [A]R
cqs 5966class (A / R)
df-ec 5967[A]R = (R “ {A})
df-qs 5971(A / R) = {y x A y = [x]R}
cmap 6019class m
cpm 6020class pm
df-map 6021m = (x V, y V {f f:y–→x})
df-pm 6022pm = (x V, y V {f (y × x) Fun f})
cen 6048class
df-en 6049 ≈ = {x, y f f:x1-1-ontoy}
cncs 6108class NC
clec 6109class c
cltc 6110class <c
cnc 6111class Nc A
cmuc 6112class ·c
ctc 6113class Tc A
c2c 6114class 2c
c3c 6115class 3c
cce 6116class c
ctcfn 6117class TcFn
df-ncs 6118 NC = (V / ≈ )
df-lec 6119c = {a, b x a y b x y}
df-ltc 6120 <c = ( ≤c I )
df-nc 6121 Nc A = [A] ≈
df-muc 6122 ·c = (m NC , n NC {a b m g n a ≈ (b × g)})
df-tc 6123 Tc A = (℩b(b NC x A b = Nc 1x))
df-2c 61242c = Nc {, V}
df-3c 61253c = Nc {, V, (V {})}
df-ce 6126c = (n NC , m NC {g ab(1a n 1b m g ≈ (am b))})
df-tcfn 6127TcFn = (x 1c Tc x)
cspac 6273class Spac
df-spac 6274 Spac = (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
  Copyright terms: Public domain W3C validator