Theorem weq 954

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

(Instead of introducing weq 954 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 953. This lets us avoid overloading the = connective, thus preventing ambiguity that causes problems in certain Metamath parsers. However, logically weq 954 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 953. 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 953	1 wff x = y

Syntax hints:   = wceq 953

This theorem is referenced by:  ax4 969  ax9o 1118  ax9 1120  a9e 1121  equid 1122  stdpc6 1123  equcomi 1124  equcom 1125  equcoms 1126  equtr 1127  equtrr 1128  equtr2 1129  equequ1 1130  equequ2 1131  elequ1 1132  elequ2 1133  ax11i 1134  ax10 1137  alequcoms 1139  nalequcoms 1140  hbae 1141  hbaes 1142  hbnae 1143  hbnaes 1144  equs3 1145  equs4 1146  equsal 1147  equsex 1148  dvelimfALT 1149  dral1 1150  dral2 1151  drex1 1152  drex2 1153  a4imt 1154  a4im 1155  a4ime 1156  a4imed 1157  cbv1 1158  cbv2 1159  cbv3 1160  cbval 1161  cbvex 1162  chvar 1163  equvini 1164  sbimi 1169  drsb1 1171  sb1 1172  sb2 1173  sbequ1 1174  sbequ2 1175  sbequ12 1177  sbequ12r 1178  sbequ12a 1179  sbid 1180  stdpc4 1181  sbf 1182  sb6x 1184  hbs1f 1185  sbequ5 1186  sbequ6 1187  sbt 1188  equsb1 1189  equsb2 1190  sbied 1191  sbie 1192  equs5a 1193  equs5e 1194  equs45f 1196  sb6f 1197  sb5f 1198  aev 1204  ax16 1205  ax17eq 1207  dveeq2 1208  ax11v2 1210  ax11a2 1211  ax11 1214  ax11b 1215  sb3 1217  sb4 1218  sb4b 1219  dfsb2 1220  dfsb3 1221  hbsb2 1222  sbequi 1223  sbequ 1224  drsb2 1225  sbi1 1227  sbequ8 1242  hbsb4 1243  hbsb4t 1244  dvelimf 1245  dvelimdf 1246  sbco 1247  sbidm 1249  sbco2 1250  sbco3 1252  sbcom 1253  sb5rf 1254  sb6rf 1255  sb9i 1258  ax11v 1260  sb56 1261  sb6 1262  sb5 1263  equid1 1264  a4v 1267  a4eiv 1269  equvin 1270  a16g 1271  a16gb 1272  cbval2 1311  cbvex2 1312  cbvald 1315  cbvexd 1316  cbvex4v 1317  cleljust 1323  equsb3lem 1324  equsb3 1325  elsb3 1326  hbs1 1327  hbsb 1328  sbcom2 1329  2sb5 1330  2sb6 1331  sb6a 1332  2sb5rf 1333  2sb6rf 1334  dfsb7 1335  sb7f 1336  sb10f 1337  sbelx 1339  sbel2x 1340  sbal1 1341  sbal 1342  exsb 1345  2exsb 1346  dveeq1 1348  sbal2 1351  ax15 1352  ax17el 1354  ax11eq 1356  ax11el 1357  ax11f 1358  ax11indn 1359  ax11indi 1360  ax11indalem 1361  ax11inda2 1363  ax11inda 1364  a12stdy1 1365  a12stdy3 1367  a12stdy4 1368  a12lem1 1369  a12lem2 1370  a12study 1371  a12studyALT 1372  euf 1377  eubid 1378  eubii 1380  hbeu1 1381  hbeu 1382  sb8eu 1383  eu1 1385  mo 1386  euex 1387  eumo0 1388  eu2 1389  eu3 1390  mo2 1393  mo3 1394  mo4f 1395  mobii 1398  eu5 1402  eu4 1403  immo 1410  moimv 1412  moanim 1420  mopick 1426  2mo 1440  2mos 1441  2eu4 1445  2eu5 1446  2eu6 1447  exists1 1450  exists2 1451  cbvrexf 10338  infi1 10347  ficli 10368  homcard 10426  fgsb2 10449  icmpmon 10587  idmon 10588

Copyright terms: Public domain