HomeHome Metamath Proof Explorer This is the GIF version.
Change to Unicode version
 
List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 2wff -. ph
wi 3wff (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 146wff (ph <-> ps)
df-bi 147|- -. (((ph <-> ps) -> -. ((ph -> ps) -> -. (ps -> ph))) -> -. (-. ((ph -> ps) -> -. (ps -> ph)) -> (ph <-> ps)))
wo 222wff (ph \/ ps)
wa 223wff (ph /\ ps)
df-or 224|- ((ph \/ ps) <-> (-. ph -> ps))
df-an 225|- ((ph /\ ps) <-> -. (ph -> -. ps))
w3o 772wff (ph \/ ps \/ ch)
w3a 773wff (ph /\ ps /\ ch)
df-3or 774|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))
df-3an 775|- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
wal 951wff A.xph
cv 952class x
wceq 953wff A = B
wcel 955wff A e. B
ax-5 957|- (A.x(ph -> ps) -> (A.xph -> A.xps))
ax-6 958|- (-. A.xph -> A.x -. A.xph)
ax-7 959|- (A.xA.yph -> A.yA.xph)
ax-gen 960|- ph   =>   |- A.xph
ax-8 961|- (x = y -> (x = z -> y = z))
ax-9 962|- -. A.x -. x = y
ax-10 963|- (A.x x = y -> A.y y = x)
ax-11 964|- (x = y -> (A.yph -> A.x(x = y -> ph)))
ax-12 965|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
ax-13 966|- (x = y -> (x e. z -> y e. z))
ax-14 967|- (x = y -> (z e. x -> z e. y))
ax-17 968|- (ph -> A.xph)
ax-4 970|- (A.xph -> ph)
ax-5o 972|- (A.x(A.xph -> ps) -> (A.xph -> A.xps))
ax-6o 975|- (-. A.x -. A.xph -> ph)
wex 977wff E.xph
df-ex 978|- (E.xph <-> -. A.x -. ph)
ax-9o 1120|- (A.x(x = y -> A.xph) -> ph)
ax-10o 1137|- (A.x x = y -> (A.xph -> A.yph))
wsbc 1167wff [A / x]ph
df-sb 1169|- ([y / x]ph <-> ((x = y -> ph) /\ E.x(x = y /\ ph)))
ax-16 1207|- (A.x x = y -> (ph -> A.xph))
ax-11o 1215|- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
ax-15 1357|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))
weu 1377wff E!xph
wmo 1378wff E*xph
df-eu 1379|- (E!xph <-> E.yA.x(ph <-> x = y))
df-mo 1380|- (E*xph <-> (E.xph -> E!xph))
ax-ext 1456|- (A.z(z e. x <-> z e. y) -> x = y)
cab 1460class {x | ph}
df-clab 1461|- (x e. {y | ph} <-> [x / y]ph)
df-cleq 1466|- (A.x(x e. y <-> x e. z) -> y = z)   =>   |- (A = B <-> A.x(x e. A <-> x e. B))
df-clel 1469|- (A e. B <-> E.x(x = A /\ x e. B))
wne 1581wff A =/= B
wnel 1582wff A e/ B
df-ne 1583|- (A =/= B <-> -. A = B)
df-nel 1584|- (A e/ B <-> -. A e. B)
wral 1641wff A.x e. A ph
wrex 1642wff E.x e. A ph
wreu 1643wff E!x e. A ph
crab 1644class {x e. A | ph}
df-ral 1645|- (A.x e. A ph <-> A.x(x e. A -> ph))
df-rex 1646|- (E.x e. A ph <-> E.x(x e. A /\ ph))
df-reu 1647|- (E!x e. A ph <-> E!x(x e. A /\ ph))
df-rab 1648|- {x e. A | ph} = {x | (x e. A /\ ph)}
cvv 1806class V
df-v 1807|- V = {x | x = x}
df-sbc 1937|- ([A / x]ph <-> A e. {x | ph})
csb 1996class [_A / x]_B
df-csb 1997|- [_A / x]_B = {y | [A / x]y e. B}
cdif 2039class (A \ B)
cun 2040class (A u. B)
cin 2041class (A i^i B)
wss 2042wff A (_ B
wpss 2043wff A (. B
df-dif 2044|- (A \ B) = {x | (x e. A /\ -. x e. B)}
df-un 2045|- (A u. B) = {x | (x e. A \/ x e. B)}
df-in 2046|- (A i^i B) = {x | (x e. A /\ x e. B)}
df-ss 2048|- (A (_ B <-> (A i^i B) = A)
df-pss 2050|- (A (. B <-> (A (_ B /\ A =/= B))
c0 2275class (/)
df-nul 2276|- (/) = (V \ V)
cif 2356class if(ph, A, B)
df-if 2357|- if(ph, A, B) = {x | ((x e. A /\ ph) \/ (x e. B /\ -. ph))}
cpw 2396class P~A
df-pw 2397|- P~A = {x | x (_ A}
csn 2404class {A}
cpr 2405class {A, B}
cop 2406class <.A, B>.
df-sn 2407|- {A} = {x | x = A}
df-pr 2408|- {A, B} = ({A} u. {B})
ctp 2409class {A, B, C}
df-tp 2410|- {A, B, C} = ({A, B} u. {C})
df-op 2411|- <.A, B>. = {{A}, {A, B}}
cuni 2498class U.A
df-uni 2499|- U.A = {x | E.y(x e. y /\ y e. A)}
cint 2528class |^|A
df-int 2529|- |^|A = {x | A.y(y e. A -> x e. y)}
ciun 2561class U_x e. A B
ciin 2562class |^|_x e. A B
df-iun 2563|- U_x e. A B = {y | E.x e. A y e. B}
df-iin 2564|- |^|_x e. A B = {y | A.x e. A y e. B}
wbr 2614wff ARB
df-br 2615|- (ARB <-> <.A, B>. e. R)
copab 2661class {<.x, y>. | ph}
df-opab 2662|- {<.x, y>. | ph} = {z | E.xE.y(z = <.x, y>. /\ ph)}
wtr 2675wff Tr A
df-tr 2676|- (Tr A <-> U.A (_ A)
ax-rep 2688|- (A.wE.yA.z(A.yph -> z = y) -> E.yA.z(z e. y <-> E.w(w e. x /\ A.yph)))
ax-sep 2698|- E.yA.x(x e. y <-> (x e. z /\ ph))
ax-nul 2705|- E.xA.y -. y e. x
ax-pow 2737|- E.yA.z(A.w(w e. z -> w e. x) -> z e. y)
ax-pr 2774|- E.zA.w((w = x \/ w = y) -> w e. z)
cep 2826class E
cid 2827class I
df-eprel 2828|- E = {<.x, y>. | x e. y}
df-id 2831|- I = {<.x, y>. | x = y}
wpo 2836wff R Po A
wor 2837wff R Or A
df-po 2838|- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
df-so 2848|- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
ax-un 2864|- E.yA.z(E.w(z e. w /\ w e. x) -> z e. y)
wfr 2912wff R Fr A
wwe 2913wff R We A
df-fr 2914|- (R Fr A <-> A.x((x (_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))
df-we 2931|- (R We A <-> (R Fr A /\ R Or A))
word 2944wff Ord A
con0 2945class On
wlim 2946wff Lim A
csuc 2947class suc A
df-ord 2948|- (Ord A <-> (Tr A /\ E We A))
df-on 2949|- On = {x | Ord x}
df-lim 2950|- (Lim A <-> (Ord A /\ A =/= (/) /\ A = U.A))
df-suc 2951|- suc A = (A u. {A})
com 3129class om
df-om 3130|- om = {x | (Ord x /\ A.y(Lim y -> x e. y))}
cxp 3166class (A X. B)
ccnv 3167class `'A
cdm 3168class dom A
crn 3169class ran A
cres 3170class (A |` B)
cima 3171class (A"B)
ccom 3172class (A o. B)
wrel 3173wff Rel A
wfun 3174wff Fun A
wfn 3175wff A Fn B
wf 3176wff F:A-->B
wf1 3177wff F:A-1-1->B
wfo 3178wff F:A-onto->B
wf1o 3179wff F:A-1-1-onto->B
cfv 3180class (F` A)
wiso 3181wff H Isom R, S (A, B)
df-xp 3182|- (A X. B) = {<.x, y>. | (x e. A /\ y e. B)}
df-rel 3183|- (Rel A <-> A (_ (V X. V))
df-cnv 3184|- `'A = {<.x, <