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 773	wff (ph \/ ps \/ ch)
w3a 774	wff (ph /\ ps /\ ch)
df-3or 775	|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
df-3an 776	|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
wal 952	wff A.xph
cv 953	class x
wceq 954	wff A = B
wcel 956	wff A e. B
ax-5 958	|- (A.x(ph -> ps) -> (A.xph -> A.xps))
ax-6 959	|- (-. A.xph -> A.x -. A.xph)
ax-7 960	|- (A.xA.yph -> A.yA.xph)
ax-gen 961	|- ph   =>   |- A.xph
ax-8 962	|- (x = y -> (x = z -> y = z))
ax-9 963	|- -. A.x -. x = y
ax-10 964	|- (A.x x = y -> A.y y = x)
ax-11 965	|- (x = y -> (A.yph -> A.x(x = y -> ph)))
ax-12 966	|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
ax-13 967	|- (x = y -> (x e. z -> y e. z))
ax-14 968	|- (x = y -> (z e. x -> z e. y))
ax-17 969	|- (ph -> A.xph)
ax-4 971	|- (A.xph -> ph)
ax-5o 973	|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
ax-6o 976	|- (-. A.x -. A.xph -> ph)
wex 978	wff E.xph
df-ex 979	|- (E.xph <-> -. A.x -. ph)
ax-9o 1121	|- (A.x(x = y -> A.xph) -> ph)
ax-10o 1138	|- (A.x x = y -> (A.xph -> A.yph))
wsbc 1168	wff [A / x]ph
df-sb 1170	|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
ax-16 1208	|- (A.x x = y -> (ph -> A.xph))
ax-11o 1216	|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
ax-15 1358	|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
weu 1378	wff E!xph
wmo 1379	wff E*xph
df-eu 1380	|- (E!xph <-> E.yA.x(ph <-> x = y))
df-mo 1381	|- (E*xph <-> (E.xph -> E!xph))
ax-ext 1457	|- (A.z(z e. x <-> z e. y) -> x = y)
cab 1461	class {x | ph}
df-clab 1462	|- (x e. {y | ph} <-> [x / y]ph)
df-cleq 1467	|- (A.x(x e. y <-> x e. z) -> y = z)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
df-clel 1470	|- (A e. B <-> E.x(x = A /\ x e. B))
wne 1582	wff A =/= B
wnel 1583	wff A e/ B
df-ne 1584	|- (A =/= B <-> -. A = B)
df-nel 1585	|- (A e/ B <-> -. A e. B)
wral 1642	wff A.x e. A ph
wrex 1643	wff E.x e. A ph
wreu 1644	wff E!x e. A ph
crab 1645	class {x e. A | ph}
df-ral 1646	|- (A.x e. A ph <-> A.x(x e. A -> ph))
df-rex 1647	|- (E.x e. A ph <-> E.x(x e. A /\ ph))
df-reu 1648	|- (E!x e. A ph <-> E!x(x e. A /\ ph))
df-rab 1649	|- {x e. A | ph} = {x | (x e. A /\ ph)}
cvv 1807	class V
df-v 1808	|- V = {x | x = x}
df-sbc 1938	|- ([A / x]ph <-> A e. {x | ph})
csb 1997	class [_A / x]_B
df-csb 1998	|- [_A / x]_B = {y | [A / x]y e. B}
cdif 2040	class (A \ B)
cun 2041	class (A u. B)
cin 2042	class (A i^i B)
wss 2043	wff A (_ B
wpss 2044	wff A (. B
df-dif 2045	|- (A \ B) = {x | (x e. A /\ -. x e. B)}
df-un 2046	|- (A u. B) = {x | (x e. A \/ x e. B)}
df-in 2047	|- (A i^i B) = {x | (x e. A /\ x e. B)}
df-ss 2049	|- (A (_ B <-> (A i^i B) = A)
df-pss 2051	|- (A (. B <-> (A (_ B /\ A =/= B))
c0 2276	class (/)
df-nul 2277	|- (/) = (V \ V)
cif 2357	class if(ph, A, B)
df-if 2358	|- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
cpw 2397	class P~A
df-pw 2398	|- P~A = {x | x (_ A}
csn 2405	class {A}
cpr 2406	class {A, B}
cop 2407	class <.A, B>.
df-sn 2408	|- {A} = {x | x = A}
df-pr 2409	|- {A, B} = ({A} u. {B})
ctp 2410	class {A, B, C}
df-tp 2411	|- {A, B, C} = ({A, B} u. {C})
df-op 2412	|- <.A, B>. = {{A}, {A, B}}
cuni 2499	class U.A
df-uni 2500	|- U.A = {x | E.y(x e. y /\ y e. A)}
cint 2529	class |^|A
df-int 2530	|- |^|A = {x | A.y(y e. A -> x e. y)}
ciun 2562	class U_x e. A B
ciin 2563	class |^|_x e. A B
df-iun 2564	|- U_x e. A B = {y | E.x e. A y e. B}
df-iin 2565	|- |^|_x e. A B = {y | A.x e. A y e. B}
wbr 2615	wff ARB
df-br 2616	|- (ARB <-> <.A, B>. e. R)
copab 2662	class {<.x, y>. | ph}
df-opab 2663	|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
wtr 2676	wff Tr A
df-tr 2677	|- (Tr A <-> U.A (_ A)
ax-rep 2689	|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
ax-sep 2699	|- E.yA.x(x e. y <-> (x e. z /\ ph))
ax-nul 2706	|- E.xA.y -. y e. x
ax-pow 2738	|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
ax-pr 2775	|- E.zA.w((w = x \/ w = y) -> w e. z)
cep 2827	class E
cid 2828	class I
df-eprel 2829	|- E = {<.x, y>. | x e. y}
df-id 2832	|- I = {<.x, y>. | x = y}
wpo 2837	wff R Po A
wor 2838	wff R Or A
df-po 2839	|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
df-so 2849	|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
ax-un 2865	|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
wfr 2914	wff R Fr A
wwe 2915	wff R We A
df-fr 2916	|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
df-we 2933	|- (R We A <-> (R Fr A /\ R Or A))
word 2946	wff Ord A
con0 2947	class On
wlim 2948	wff Lim A
csuc 2949	class suc A
df-ord 2950	|- (Ord A <-> (Tr A /\ E We A))
df-on 2951	|- On = {x | Ord x}
df-lim 2952	|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
df-suc 2953	|- suc A = (A u. {A})
com 3131	class om
df-om 3132	|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
cxp 3168	class (A X. B)
ccnv 3169	class `'A
cdm 3170	class dom A
crn 3171	class ran A
cres 3172	class (A |` B)
cima 3173	class (A"B)
ccom 3174	class (A o. B)
wrel 3175	wff Rel A
wfun 3176	wff Fun A
wfn 3177	wff A Fn B
wf 3178	wff F:A-->B
wf1 3179	wff F:A-1-1->B
wfo 3180	wff F:A-onto->B
wf1o 3181	wff F:A-1-1-onto->B
cfv 3182	class (F` A)
wiso 3183	wff H Isom R, S (A, B)
df-xp 3184	|- (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}
df-rel 3185	|- (Rel A <-> A (_ (V X. V))
df-cnv 3186	|- `'A = {<.x, <