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 776	wff (ph \/ ps \/ ch)
w3a 777	wff (ph /\ ps /\ ch)
df-3or 778	|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
df-3an 779	|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
wal 956	wff A.xph
cv 957	class x
wceq 958	wff A = B
wcel 960	wff A e. B
ax-5 962	|- (A.x(ph -> ps) -> (A.xph -> A.xps))
ax-6 963	|- (-. A.xph -> A.x -. A.xph)
ax-7 964	|- (A.xA.yph -> A.yA.xph)
ax-gen 965	|- ph   =>   |- A.xph
ax-8 966	|- (x = y -> (x = z -> y = z))
ax-9 967	|- -. A.x -. x = y
ax-10 968	|- (A.x x = y -> A.y y = x)
ax-11 969	|- (x = y -> (A.yph -> A.x(x = y -> ph)))
ax-12 970	|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
ax-13 971	|- (x = y -> (x e. z -> y e. z))
ax-14 972	|- (x = y -> (z e. x -> z e. y))
ax-17 973	|- (ph -> A.xph)
ax-4 975	|- (A.xph -> ph)
ax-5o 977	|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
ax-6o 980	|- (-. A.x -. A.xph -> ph)
wex 982	wff E.xph
df-ex 983	|- (E.xph <-> -. A.x -. ph)
ax-9o 1125	|- (A.x(x = y -> A.xph) -> ph)
ax-10o 1142	|- (A.x x = y -> (A.xph -> A.yph))
wsbc 1172	wff [A / x]ph
df-sb 1174	|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
ax-16 1212	|- (A.x x = y -> (ph -> A.xph))
ax-11o 1220	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
ax-15 1362	|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
weu 1382	wff E!xph
wmo 1383	wff E*xph
df-eu 1384	|- (E!xph <-> E.yA.x(ph <-> x = y))
df-mo 1385	|- (E*xph <-> (E.xph -> E!xph))
ax-ext 1462	|- (A.z(z e. x <-> z e. y) -> x = y)
cab 1466	class {x | ph}
df-clab 1467	|- (x e. {y | ph} <-> [x / y]ph)
df-cleq 1472	|- (A.x(x e. y <-> x e. z) -> y = z)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
df-clel 1475	|- (A e. B <-> E.x(x = A /\ x e. B))
wne 1588	wff A =/= B
wnel 1589	wff A e/ B
df-ne 1590	|- (A =/= B <-> -. A = B)
df-nel 1591	|- (A e/ B <-> -. A e. B)
wral 1648	wff A.x e. A ph
wrex 1649	wff E.x e. A ph
wreu 1650	wff E!x e. A ph
crab 1651	class {x e. A | ph}
df-ral 1652	|- (A.x e. A ph <-> A.x(x e. A -> ph))
df-rex 1653	|- (E.x e. A ph <-> E.x(x e. A /\ ph))
df-reu 1654	|- (E!x e. A ph <-> E!x(x e. A /\ ph))
df-rab 1655	|- {x e. A | ph} = {x | (x e. A /\ ph)}
cvv 1814	class V
df-v 1815	|- V = {x | x = x}
df-sbc 1945	|- ([A / x]ph <-> A e. {x | ph})
csb 2004	class [_A / x]_B
df-csb 2005	|- [_A / x]_B = {y | [A / x]y e. B}
cdif 2047	class (A \ B)
cun 2048	class (A u. B)
cin 2049	class (A i^i B)
wss 2050	wff A (_ B
wpss 2051	wff A (. B
df-dif 2052	|- (A \ B) = {x | (x e. A /\ -. x e. B)}
df-un 2053	|- (A u. B) = {x | (x e. A \/ x e. B)}
df-in 2054	|- (A i^i B) = {x | (x e. A /\ x e. B)}
df-ss 2056	|- (A (_ B <-> (A i^i B) = A)
df-pss 2058	|- (A (. B <-> (A (_ B /\ A =/= B))
c0 2283	class (/)
df-nul 2284	|- (/) = (V \ V)
cif 2365	class if(ph, A, B)
df-if 2366	|- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
cpw 2405	class P~A
df-pw 2406	|- P~A = {x | x (_ A}
csn 2413	class {A}
cpr 2414	class {A, B}
cop 2415	class <.A, B>.
df-sn 2416	|- {A} = {x | x = A}
df-pr 2417	|- {A, B} = ({A} u. {B})
ctp 2418	class {A, B, C}
df-tp 2419	|- {A, B, C} = ({A, B} u. {C})
df-op 2420	|- <.A, B>. = {{A}, {A, B}}
cuni 2507	class U.A
df-uni 2508	|- U.A = {x | E.y(x e. y /\ y e. A)}
cint 2537	class |^|A
df-int 2538	|- |^|A = {x | A.y(y e. A -> x e. y)}
ciun 2570	class U_x e. A B
ciin 2571	class |^|_x e. A B
df-iun 2572	|- U_x e. A B = {y | E.x e. A y e. B}
df-iin 2573	|- |^|_x e. A B = {y | A.x e. A y e. B}
wbr 2624	wff ARB
df-br 2625	|- (ARB <-> <.A, B>. e. R)
copab 2671	class {<.x, y>. | ph}
df-opab 2672	|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
wtr 2685	wff Tr A
df-tr 2686	|- (Tr A <-> U.A (_ A)
ax-rep 2698	|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
ax-sep 2708	|- E.yA.x(x e. y <-> (x e. z /\ ph))
ax-nul 2715	|- E.xA.y -. y e. x
ax-pow 2748	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
ax-pr 2785	|- E.zA.w((w = x \/ w = y) -> w e. z)
cep 2836	class E
cid 2837	class I
df-eprel 2838	|- E = {<.x, y>. | x e. y}
df-id 2841	|- I = {<.x, y>. | x = y}
wpo 2844	wff R Po A
wor 2845	wff R Or A
df-po 2846	|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
df-so 2856	|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
ax-un 2872	|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
wfr 2921	wff R Fr A
wwe 2922	wff R We A
df-fr 2923	|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
df-we 2940	|- (R We A <-> (R Fr A /\ R Or A))
word 2953	wff Ord A
con0 2954	class On
wlim 2955	wff Lim A
csuc 2956	class suc A
df-ord 2957	|- (Ord A <-> (Tr A /\ E We A))
df-on 2958	|- On = {x | Ord x}
df-lim 2959	|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
df-suc 2960	|- suc A = (A u. {A})
com 3137	class om
df-om 3138	|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
cxp 3174	class (A X. B)
ccnv 3175	class `'A
cdm 3176	class dom A
crn 3177	class ran A
cres 3178	class (A |` B)
cima 3179	class (A"B)
ccom 3180	class (A o. B)
wrel 3181	wff Rel A
wfun 3182	wff Fun A
wfn 3183	wff A Fn B
wf 3184	wff F:A-->B
wf1 3185	wff F:A-1-1->B
wfo 3186	wff F:A-onto->B
wf1o 3187	wff F:A-1-1-onto->B
cfv 3188	class (F` A)
wiso 3189	wff H Isom R, S (A, B)
df-xp 3190