mmdefinitions - Metamath Proof Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wn 2	wff -. ph
wi 3	wff (ph -> ps)
ax-1 4	|- (ph -> (ps -> ph))
ax-2 5	|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))
ax-3 6	|- ((-. ph -> -. ps) -> (ps -> ph))
ax-mp 7	|- ph   &   |- (ph -> ps)   =>   |- ps
wb 146	wff (ph <-> ps)
df-bi 147	|- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
wo 222	wff (ph \/ ps)
wa 223	wff (ph /\ ps)
df-or 224	|- ((ph \/ ps) <-> (-. ph -> ps))
df-an 225	|- ((ph /\ ps) <-> -. (ph -> -. ps))
w3o 771	wff (ph \/ ps \/ ch)
w3a 772	wff (ph /\ ps /\ ch)
df-3or 773	|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
df-3an 774	|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
wal 950	wff A.xph
ax-4 951	|- (A.xph -> ph)
ax-5 952	|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
ax-6 953	|- (-. A.x -. A.xph -> ph)
ax-7 954	|- (A.xA.yph -> A.yA.xph)
ax-gen 955	|- ph   =>   |- A.xph
wex 956	wff E.xph
df-ex 957	|- (E.xph <-> -. A.x -. ph)
cv 1098	class x
wceq 1099	wff A = B
ax-8 1101	|- (x = y -> (x = z -> y = z))
ax-9 1102	|- -. A.x -. x = y
ax-10 1103	|- (A.x x = y -> (A.xph -> A.yph))
ax-12 1104	|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
wcel 1105	wff A e. B
ax-13 1107	|- (x = y -> (x e. z -> y e. z))
ax-14 1108	|- (x = y -> (z e. x -> z e. y))
ax-15 1109	|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
wsbc 1153	wff [A / x]ph
df-sb 1155	|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
ax-11 1180	|- (x = y -> (A.yph -> A.x(x = y -> ph)))
ax-17 1190	|- (ph -> A.xph)
ax-16 1194	|- (A.x x = y -> (ph -> A.xph))
ax-11o 1202	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
weu 1357	wff E!xph
wmo 1358	wff E*xph
df-eu 1359	|- (E!xph <-> E.yA.x(ph <-> x = y))
df-mo 1360	|- (E*xph <-> (E.xph -> E!xph))
ax-ext 1436	|- (A.z(z e. x <-> z e. y) -> x = y)
cab 1440	class {x | ph}
df-clab 1441	|- (x e. {y | ph} <-> [x / y]ph)
df-cleq 1446	|- (A.x(x e. y <-> x e. z) -> y = z)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
df-clel 1449	|- (A e. B <-> E.x(x = A /\ x e. B))
wne 1561	wff A =/= B
wnel 1562	wff A e/ B
df-ne 1563	|- (A =/= B <-> -. A = B)
df-nel 1564	|- (A e/ B <-> -. A e. B)
wral 1621	wff A.x e. A ph
wrex 1622	wff E.x e. A ph
wreu 1623	wff E!x e. A ph
crab 1624	class {x e. A | ph}
df-ral 1625	|- (A.x e. A ph <-> A.x(x e. A -> ph))
df-rex 1626	|- (E.x e. A ph <-> E.x(x e. A /\ ph))
df-reu 1627	|- (E!x e. A ph <-> E!x(x e. A /\ ph))
df-rab 1628	|- {x e. A | ph} = {x | (x e. A /\ ph)}
cvv 1786	class V
df-v 1787	|- V = {x | x = x}
df-sbc 1913	|- ([A / x]ph <-> A e. {x | ph})
csb 1972	class [_A / x]_B
df-csb 1973	|- [_A / x]_B = {y | [A / x]y e. B}
cdif 2015	class (A \ B)
cun 2016	class (A u. B)
cin 2017	class (A i^i B)
wss 2018	wff A (_ B
wpss 2019	wff A (. B
df-dif 2020	|- (A \ B) = {x | (x e. A /\ -. x e. B)}
df-un 2021	|- (A u. B) = {x | (x e. A \/ x e. B)}
df-in 2022	|- (A i^i B) = {x | (x e. A /\ x e. B)}
df-ss 2024	|- (A (_ B <-> (A i^i B) = A)
df-pss 2026	|- (A (. B <-> (A (_ B /\ A =/= B))
c0 2251	class (/)
df-nul 2252	|- (/) = (V \ V)
cif 2332	class if(ph, A, B)
df-if 2333	|- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
cpw 2372	class P~A
df-pw 2373	|- P~A = {x | x (_ A}
csn 2380	class {A}
cpr 2381	class {A, B}
cop 2382	class <.A, B>.
df-sn 2383	|- {A} = {x | x = A}
df-pr 2384	|- {A, B} = ({A} u. {B})
ctp 2385	class {A, B, C}
df-tp 2386	|- {A, B, C} = ({A, B} u. {C})
df-op 2387	|- <.A, B>. = {{A}, {A, B}}
cuni 2471	class U.A
df-uni 2472	|- U.A = {x | E.y(x e. y /\ y e. A)}
cint 2501	class |^|A
df-int 2502	|- |^|A = {x | A.y(y e. A -> x e. y)}
ciun 2534	class U_x e. A B
ciin 2535	class |^|_x e. A B
df-iun 2536	|- U_x e. A B = {y | E.x e. A y e. B}
df-iin 2537	|- |^|_x e. A B = {y | A.x e. A y e. B}
wbr 2587	wff ARB
df-br 2588	|- (ARB <-> <.A, B>. e. R)
copab 2634	class {<.x, y>. | ph}
df-opab 2635	|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
wtr 2648	wff Tr A
df-tr 2649	|- (Tr A <-> U.A (_ A)
ax-rep 2661	|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
ax-sep 2671	|- E.yA.x(x e. y <-> (x e. z /\ ph))
ax-nul 2678	|- E.xA.y -. y e. x
ax-pow 2710	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
ax-pr 2747	|- E.zA.w((w = x \/ w = y) -> w e. z)
cep 2792	class E
cid 2793	class I
df-eprel 2794	|- E = {<.x, y>. | x e. y}
df-id 2797	|- I = {<.x, y>. | x = y}
wpo 2802	wff R Po A
wor 2803	wff R Or A
df-po 2804	|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
df-so 2814	|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
ax-un 2830	|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
wfr 2878	wff R Fr A
wwe 2879	wff R We A
df-fr 2880	|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
df-we 2897	|- (R We A <-> (R Fr A /\ R Or A))
word 2910	wff Ord A
con0 2911	class On
wlim 2912	wff Lim A
csuc 2913	class suc A
df-ord 2914	|- (Ord A <-> (Tr A /\ E We A))
df-on 2915	|- On = {x | Ord x}
df-lim 2916	|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
df-suc 2917	|- suc A = (A u. {A})
com 3094	class om
df-om 3095	|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
cxp 3131	class (A X. B)
ccnv 3132	class `'A
cdm 3133	class dom A
crn 3134	class ran A
cres 3135	class (A |` B)
cima 3136	class (A"B)
ccom 3137	class (A o. B)
wrel 3138	wff Rel A
wfun 3139	wff Fun A
wfn 3140	wff A Fn B
wf 3141	wff F:A-->B
wf1 3142	wff F:A-1-1->B
wfo 3143	wff F:A-onto->B
wf1o 3144	wff F:A-1-1-onto->B
cfv 3145	class (F` A)
wiso 3146	wff H Isom R, S (A, B)
df-xp 3147	|- (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}
df-rel 3148	|- (Rel A <-> A (_ (V X. V))
df-cnv 3149	|- `'A = {<.x, y>. | yAx}
df-co 3150	|- (A o. B) = {<.x, y>. | E.z(xBz /\ zAy)}
df-dm 3151	|- dom A = {x | E.y xAy}
df-rn 3152	|- ran A = dom `' A
df-res 3153	|- (A |` B) = (A i^i (