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 173wff (φψ)
df-bi 174 ¬ (((φψ) → ¬ ((φψ) → ¬ (ψφ))) → ¬ (¬ ((φψ) → ¬ (ψφ)) → (φψ)))
wo 354wff (φ ψ)
wa 355wff (φ ψ)
df-or 356((φ ψ) ↔ (¬ φψ))
df-an 357((φ ψ) ↔ ¬ (φ → ¬ ψ))
w3o 883wff (φ ψ χ)
w3a 884wff (φ ψ χ)
df-3or 885((φ ψ χ) ↔ ((φ ψ) χ))
df-3an 886((φ ψ χ) ↔ ((φ ψ) χ))
ax-meredith 1230(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
wnand 1258wff (φ ψ)
df-nand 1259((φ ψ) ↔ ¬ (φ ψ))
wtru 1298wff
wfal 1299wff
df-tru 1301( ⊤ ↔ (φφ))
df-fal 1302( ⊥ ↔ ¬ ⊤ )
wal 1322wff xφ
ax-5 1323(x(φψ) → (xφxψ))
ax-6 1324xφx ¬ xφ)
ax-7 1325(xyφyxφ)
ax-gen 1326φ       xφ
wex 1327wff xφ
df-ex 1328(xφ ↔ ¬ x ¬ φ)
cv 1397class x
wceq 1398wff A = B
wcel 1400wff A B
ax-8 1402(x = y → (x = zy = z))
ax-10 1403(x x = yy y = x)
ax-11 1404(x = y → (yφx(x = yφ)))
ax-12 1405z z = x → (¬ z z = y → (x = yz x = y)))
ax-13 1406(x = y → (x zy z))
ax-14 1407(x = y → (z xz y))
ax-17 1413(φxφ)
ax-9 1424 ¬ x ¬ x = y
ax-4 1429(xφφ)
ax-5o 1431(x(xφψ) → (xφxψ))
ax-6o 1434x ¬ xφφ)
ax-9o 1519(x(x = yxφ) → φ)
ax-10o 1538(x x = y → (xφyφ))
wsbc 1566wff [A / x]φ
df-sb 1568([y / x]φ ↔ ((x = yφ) x(x = y φ)))
ax-16 1606(x x = y → (φxφ))
ax-11o 1616x x = y → (x = y → (φx(x = yφ))))
ax-15 1769z z = x → (¬ z z = y → (x yz x y)))
weu 1791wff ∃!xφ
wmo 1792wff ∃*xφ
df-eu 1795(∃!xφyx(φx = y))
df-mo 1796(∃*xφ ↔ (xφ∃!xφ))
ax-ext 1877(z(z xz y) → x = y)
cab 1882class {x φ}
df-clab 1883(x {y φ} ↔ [x / y]φ)
df-cleq 1888(x(x yx z) → y = z)       (A = Bx(x Ax B))
df-clel 1891(A Bx(x = A x B))
wne 2012wff AB
wnel 2013wff A B
df-ne 2014(AB ↔ ¬ A = B)
df-nel 2015(A B ↔ ¬ A B)
wral 2103wff x A φ
wrex 2104wff x A φ
wreu 2105wff ∃!x A φ
crab 2106class {x A φ}
df-ral 2107(x A φx(x Aφ))
df-rex 2108(x A φx(x A φ))
df-reu 2109(∃!x A φ∃!x(x A φ))
df-rab 2110{x A φ} = {x (x A φ)}
cvv 2300class V
df-v 2302V = {x x = x}
df-sbc 2469([A / x]φA {x φ})
csb 2550class [A / x]B
df-csb 2551[A / x]B = {y [A / x]y B}
cnin 2606class (AB)
ccompl 2607class A
cdif 2608class (A B)
cun 2609class (AB)
cin 2610class (AB)
csymdif 2611class (AB)
df-nin 2613(AB) = {x (x A x B)}
df-compl 2614A = (AA)
df-in 2615(AB) = ∼ (AB)
df-un 2616(AB) = ( ∼ A ⩃ ∼ B)
df-dif 2617(A B) = (A ∩ ∼ B)
df-symdif 2618(AB) = ((A B) ∪ (B A))
c0 2726class
df-nul 2727 = ∼ V
csn 2803class {A}
cpr 2804class {A, B}
ctp 2805class {A, B, C}
df-sn 2807{A} = {x x = A}
df-pr 2808{A, B} = ({A} ∪ {B})
df-tp 2809{A, B, C} = ({A, B} ∪ {C})
copk 2862class A, B
df-opk 2863A, B⟫ = {{A}, {A, B}}
wss 2874wff A B
wpss 2875wff A B
df-ss 2876(A B ↔ (AB) = A)
df-pss 2878(A B ↔ (A B AB))
cuni 3037class A
df-uni 3038A = {x y(x y y A)}
cint 3071class A
df-int 3072A = {x y(y Ax y)}
cif 3108class if(φ, A, B)
df-if 3109 if(φ, A, B) = {x ((x A φ) (x B ¬ φ))}
cpw 3165class A
df-pw 3167A = {x x A}
ax-nin 3180zw(w z ↔ (w x w y))
ax-xp 3181yz(z ywt(z = ⟪w, t t x))
ax-cnv 3182yzw(⟪z, w y ↔ ⟪w, z x)
ax-1c 3183xy(y xzw(w yw = z))
ax-sset 3184xyz(⟪y, z xw(w yw z))
ax-si 3185yzw(⟪{z}, {w}⟫ y ↔ ⟪z, w x)
ax-ins2 3186yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, t x)
ax-ins3 3187yzwt(⟪{{z}}, ⟪w, t⟫⟫ y ↔ ⟪z, w x)
ax-typlower 3188yz(z yww, {z}⟫ x)
ax-sn 3189yz(z yz = x)
cuni1 3237class 1A
c1c 3238class 1c
cpw1 3239class 1A
df-1c 32401c = {x y x = {y}}
df-pw1 32411A = (A ∩ 1c)
df-uni1 32421A = (A ∩ 1c)
cxpk 3278class (A ×k B)
ccnvk 3279class kA
cins2k 3280class Ins2k A
cins3k 3281class Ins3k A
cp6 3282class P6 A
cimak 3283class (Ak B)
ccomk 3284class (A k B)
csik 3285class SIk A
cimagek 3286class ImagekA
cssetk 3287class SSetk
cidk 3288class Ik
df-xpk 3289(A ×k B) = {x yz(x = ⟪y, z (y A z B))}
df-cnvk 3290kA = {x yz(x = ⟪y, zz, y A)}
df-ins2k 3291 Ins2k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, v A))}
df-ins3k 3292 Ins3k A = {x yz(x = ⟪y, z tuv(y = {{t}} z = ⟪u, vt, u A))}
df-imak 3293(Ak B) = {x y By, x A}
df-cok 3294(A k B) = (( Ins2k AIns3k kB) “k V)
df-p6 3295 P6 A = {x (V ×k {{x}}) A}
df-sik 3296 SIk A = {x yz(x = ⟪y, z tu(y = {t} z = {u} t, u A))}
df-ssetk 3297 SSetk = {x yz(x = ⟪y, z y z)}
df-imagek 3298ImagekA = ((V ×k V) (( Ins2k SSetkIns3k ( SSetk k k SIk A)) “k 111c))
df-idk 3299 Ik = {x yz(x = ⟪y, z y = z)}
cio 3448class (℩xφ)
df-iota 3450(℩xφ) = {y {x φ} = {y}}
cnnc 3481class Nn
c0c 3482class 0c
cplc 3483class (A +c B)
cfin 3484class Fin
df-0c 34850c = {}
df-addc 3486(A +c B) = {x y A z B ((yz) = x = (yz))}
df-nnc 3487 Nn = {b (0c b y b (y +c 1c) b)}
df-fin 3488 Fin = Nn
clefin 3539class fin
cltfin 3540class <fin
cncfin 3541class Ncfin A
ctfin 3542class Tfin A
cevenfin 3543class Evenfin
coddfin 3544class Oddfin
wsfin 3545wff Sfin (A, B)
cspfin 3546class Spfin
df-lefin 3547fin = {x yz(x = ⟪y, z w Nn z = (y +c w))}
df-ltfin 3548 <fin = {x mn(x = ⟪m, n (m p Nn n = ((m +c p) +c 1c)))}
df-ncfin 3549 Ncfin A = (℩x(x Nn A x))
df-tfin 3550 Tfin M = if(M = , , (℩n(n Nn a M 1a n)))
df-evenfin 3551 Evenfin = {x (n Nn x = (n +c n) x)}
df-oddfin 3552 Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
df-sfin 3553( Sfin (M, N) ↔ (M Nn N Nn a(1a M a N)))
df-spfin 3554 Spfin = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
cop 3669class A, B
cphi 3670class Phi A
cproj1 3671class Proj1 A
cproj2 3672class Proj2 A
df-phi 3673 Phi A = {y x A y = if(x Nn , (x +c 1c), x)}
df-op 3674A, B = ({x y A x = Phi y} ∪ {x y B x = ( Phi y ∪ {0c})})
df-proj1 3675 Proj1 A = {x Phi x A}
df-proj2 3676 Proj2 A = {x ( Phi x ∪ {0c}) A}
copab 3722class {x, y φ}
df-opab 3723{x, y φ} = {z xy(z = x, y φ)}
wbr 3736wff ARB
df-br 3737(ARBA, B R)
c1st 3815class 1st
cswap 3816class Swap
csset 3817class SSet
csi 3818class SI A
ccom 3819class (A B)
cima 3820class (AB)
df-1st 38211st = {x, y z x = y, z}
df-swap 3822 Swap = {x, y zw(x = z, w y = w, z)}
df-sset 3823 SSet = {x, y x y}
df-co 3824(A B) = {x, y z(xBz zAy)}
df-ima 3825(AB) = {x y B yAx}
df-si 3826 SI A = {x, y zw(x = {z} y = {w} zAw)}
ciun 3860class x A B
ciin 3861class x A B
df-iun 3862x A B = {y x A y B}
df-iin 3863x A B = {y x A y B}
cep 3934class E
cid 3935class I
df-eprel 3936 E = {x, y x y}
df-id 3939 I = {x, y x = y}
cxp 3942class (A × B)
ccnv 3943class A
cdm 3944class dom A
crn 3945class ran A
cres 3946class (A B)
wrel 3947wff Rel A
wfun 3948wff Fun A
wfn 3949wff A Fn B
wf 3950wff F:A–→B
wf1 3951wff F:A1-1B
wfo 3952wff F:AontoB
wf1o 3953wff F:A1-1-ontoB
cfv 3954class (FA)
wiso 3955wff H Isom R, S (A, B)
c2nd 3956class 2nd
df-xp 3957(A × B) = {x, y (x A y B)}
df-rel 3958(Rel AA (V × V))
df-cnv 3959A = {x, y yAx}
df-rn 3960ran A = (A “ V)
df-dm 3961dom A = ran A
df-res 3962(A B) = (A ∩ (B × V))
df-fun 3963(Fun A ↔ (Rel A (A A) I ))
df-fn 3964(A Fn B ↔ (Fun A dom A = B))
df-f 3965(F:A–→B ↔ (F Fn A ran F B))
df-f1 3966(F:A1-1B ↔ (F:A–→B Fun F))
df-fo 3967(F:AontoB ↔ (F Fn A ran F = B))
df-f1o 3968(F:A1-1-ontoB ↔ (F:A1-1B F:AontoB))
df-fv 3969(FA) = (℩xAFx)
df-iso 3970(H Isom R, S (A, B) ↔ (H:A1-1-ontoB x A y A (xRy ↔ (Hx)S(Hy))))
df-2nd 39712nd = {x, y z x = z, y}
co 4766class (AFB)
copab2 4767class {x, y, z φ}
df-ov 4768(AFB) = (FA, B)
df-oprab 4769{x, y, z φ} = {w xyz(w = x, y, z φ)}
cmpt 4893class (x A B)
cmpt2 4894class (x A, y B C)
df-mpt 4895(x A B) = {x, y (x A y = B)}
df-mpt2 4896(x A, y B C) = {x, y, z ((x A y B) z = C)}
ctxp 4962class (AB)
cpprod 4963class PProd (A, B)
cfix 4964class Fix A
cimage 4965class ImageA
ccup 4966class Cup
cdisj 4967class Disj
caddcfn 4968class AddC
cins2 4969class Ins2 A
cins3 4970class Ins3 A
cins4 4971class Ins4 A
csi3 4972class SI3 A
cfuns 4973class Funs
cfns 4974class Fns
ccross 4975class Cross
cpw1fn 4976class Pw1Fn
cfullfun 4977class FullFun F
df-txp 4978(AB) = ((1st A) ∩ (2nd B))
df-pprod 4979 PProd (A, B) = ((A 1st ) ⊗ (B 2nd ))
df-fix 4980 Fix A = ran (A ∩ I )
df-cup 4981 Cup = (x V, y V (xy))
df-disj 4982 Disj = {x, y (xy) = }
df-addcfn 4983 AddC = (x V, y V (x +c y))
df-ins2 4984 Ins2 A = (V ⊗ A)
df-ins3 4985 Ins3 A = (A ⊗ V)
df-image 4986ImageA = ((V × V) (( Ins2 SSet Ins3 ( SSet SI A)) “ 1c))
df-ins4 4987 Ins4 A = ((1st ⊗ ((1st 2nd ) ⊗ ((1st 2nd ) 2nd ))) “ A)
df-si3 4988 SI3 A = (( SI 1st ⊗ ( SI (1st 2nd ) ⊗ SI (2nd 2nd ))) “ 1A)
df-funs 4989 Funs = {f Fun f}
df-fns 4990 Fns = {f, a f Fn a}
df-cross 4991 Cross = (x V, y V (x × y))
df-pw1fn 4992 Pw1Fn = (x 1c 1x)
df-fullfun 4993 FullFun F = ((( I F) ( ∼ I F)) ∪ ( ∼ dom (( I F) ( ∼ I F)) × {}))
cclos1 5085class Clos1 (A, R)
df-clos1 5086 Clos1 (S, R) = {a (S a (Ra) a)}
ctrans 5099class Trans
cref 5100class Ref
cantisym 5101class Antisym
cpartial 5102class Po
cconnex 5103class Connex
cstrict 5104class Or
cfound 5105class Fr
cwe 5106class We
cext 5107class Ext
csym 5108class Sym
cer 5109class Er
df-trans 5110 Trans = {r, a x a y a z a ((xry yrz) → xrz)}
df-ref 5111 Ref = {r, a x a xrx}
df-antisym 5112 Antisym = {r, a x a y a ((xry yrx) → x = y)}
df-partial 5113 Po = (( RefTrans ) ∩ Antisym )
df-connex 5114 Connex = {r, a x a y a (xry yrx)}
df-strict 5115 Or = ( PoConnex )
df-found 5116 Fr = {r, a x((x a x) → z x y x (yrzy = z))}
df-we 5117 We = ( OrFr )
df-ext 5118 Ext = {r, a x a y a (z a (zrxzry) → x = y)}
df-sym 5119 Sym = {r, a x a y a (xryyrx)}
df-er 5120 Er = ( SymTrans )
cec 5156class [A]R
cqs 5157class (A / R)
df-ec 5158[A]R = (R “ {A})
df-qs 5162(A / R) = {y x A y = [x]R}
cmap 5211class m
cpm 5212class pm
df-map 5213m = (x V, y V {f f:y–→x})
df-pm 5214pm = (x V, y V {f (y × x) Fun f})
cen 5240class
df-en 5241 ≈ = {x, y f f:x1-1-ontoy}
cncs 5300class NC
clec 5301class c
cltc 5302class <c
cnc 5303class Nc A
cmuc 5304class ·c
ctc 5305class Tc A
c2c 5306class 2c
c3c 5307class 3c
cce 5308class c
ctcfn 5309class TcFn
df-ncs 5310 NC = (V / ≈ )
df-lec 5311c = {a, b x a y b x y}
df-ltc 5312 <c = ( ≤c I )
df-nc 5313 Nc A = [A] ≈
df-muc 5314 ·c = (m NC , n NC {a b m g n a ≈ (b × g)})
df-tc 5315 Tc A = (℩b(b NC x A b = Nc 1x))
df-2c 53162c = Nc {, V}
df-3c 53173c = Nc {, V, (V {})}
df-ce 5318c = (n NC , m NC {g ab(1a n 1b m g ≈ (am b))})
df-tcfn 5319TcFn = (x 1c Tc x)
cspac 5465class Spac
df-spac 5466 Spac = (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
  Copyright terms: Public domain W3C validator