Theorem weq 1100

Description: Extend wff definition to include atomic formulas using the equality predicate.

(Instead of introducing weq 1100 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1099. This lets us avoid overloading the = connective, thus preventing ambiguity that causes problems in certain Metamath parsers. However, logically weq 1100 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1099. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)

Assertion

Ref	Expression
weq	wff x = y

Proof of Theorem weq

Step	Hyp	Ref	Expression
1		wceq 1099	1 wff x = y

Syntax hints:   = wceq 1099

This theorem is referenced by:  ax9 1110  ax9a 1111  a9e 1112  equid 1113  stdpc6 1114  equcomi 1115  equcom 1116  equcoms 1117  equtr 1118  equtrr 1119  equtr2 1120  equequ1 1121  equequ2 1122  elequ1 1123  elequ2 1124  alequcom 1125  alequcoms 1126  nalequcoms 1127  hbae 1128  hbaes 1129  hbnae 1130  hbnaes 1131  equs3 1132  equs4 1133  equsal 1134  equsex 1135  dvelimfALT 1136  dral1 1137  dral2 1138  drex1 1139  drex2 1140  a4at 1141  a4a 1142  a4c 1143  a4c1 1144  cbv1 1145  cbv2 1146  cbv3 1147  cbval 1148  cbvex 1149  chvar 1150  equvini 1151  sbimi 1156  drsb1 1158  sb1 1159  sb2 1160  sbequ1 1161  sbequ2 1162  sbequ12 1164  sbequ12r 1165  sbequ12a 1166  sbid 1167  stdpc4 1168  sbf 1169  sb6x 1171  hbs1f 1172  sbequ5 1173  sbequ6 1174  sbt 1175  equsb1 1176  equsb2 1177  sbied 1178  sbie 1179  equs5a 1181  equs5e 1182  equs45f 1184  sb6f 1185  aev 1192  ax16 1193  ax17eq 1195  ax17el 1196  dveeq2 1197  ax11v2 1199  ax11a2 1200  ax11 1203  ax11b 1204  sb3 1206  sb4 1207  sb4b 1208  dfsb2 1209  dfsb3 1210  hbsb2 1211  sbequi 1212  sbequ 1213  drsb2 1214  sbi1 1216  sbequ8 1231  hbsb4 1232  hbsb4t 1233  dvelimf 1234  dvelimdf 1235  sbco 1236  sbidm 1238  sbco2 1239  sbco3 1241  sbcom 1242  sb5rf 1243  sb6rf 1244  sb9i 1247  ax11v 1249  sb56 1250  sb6 1251  sb5 1252  equid1 1253  a4b1 1254  a4w1 1256  equvin 1257  a16g 1258  a16gb 1259  cbval2 1298  cbvex2 1299  cbvald 1302  cbvexd 1303  cbvex4v 1304  cleljust 1310  equsb3lem 1311  equsb3 1312  elsb3 1313  hbs1 1314  hbsb 1315  sbcom2 1316  2sb5 1317  2sb6 1318  sb6a 1319  2sb5rf 1320  2sb6rf 1321  sb7 1322  sb7f 1323  sb10f 1324  sbelx 1326  sbel2x 1327  sbal1 1328  sbal 1329  exsb 1332  2exsb 1333  dveeq1 1335  sbal2 1338  ax15 1339  ax11eq 1340  ax11el 1341  ax11f 1342  ax11indn 1343  ax11indi 1344  ax11indalem 1345  ax11inda2 1347  ax11inda 1348  a12stdy1 1349  a12stdy3 1351  a12stdy4 1352  a12lem1 1353  a12lem2 1354  a12study 1355  a12studyALT 1356  euf 1361  eubid 1362  eubii 1364  hbeu1 1365  hbeu 1366  sb8eu 1367  eu1 1369  mo 1370  euex 1371  eumo0 1372  eu2 1373  eu3 1374  mo2 1377  mo3 1378  mo4f 1379  mobii 1382  eu5 1386  eu4 1387  immo 1394  moimv 1396  moanim 1404  mopick 1410  2mo 1424  2mos 1425  2eu4 1429  2eu5 1430  2eu6 1431  exists1 1434  exists2 1435  cbvrexf 8698  infi1 8706  ficli 8727  fgsb2 8799  icmpmon 8937

Copyright terms: Public domain