Theorem weq 955

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

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

Syntax hints:   = wceq 954

This theorem is referenced by:  ax4 970  ax9o 1120  ax9 1122  a9e 1123  equid 1124  stdpc6 1125  equcomi 1126  equcom 1127  equcoms 1128  equtr 1129  equtrr 1130  equtr2 1131  equequ1 1132  equequ2 1133  elequ1 1134  elequ2 1135  ax11i 1136  ax10 1139  alequcoms 1141  nalequcoms 1142  hbae 1143  hbaes 1144  hbnae 1145  hbnaes 1146  equs3 1147  equs4 1148  equsal 1149  equsex 1150  dvelimfALT 1151  dral1 1152  dral2 1153  drex1 1154  drex2 1155  a4imt 1156  a4im 1157  a4ime 1158  a4imed 1159  cbv1 1160  cbv2 1161  cbv3 1162  cbval 1163  cbvex 1164  chvar 1165  equvini 1166  sbimi 1171  drsb1 1173  sb1 1174  sb2 1175  sbequ1 1176  sbequ2 1177  sbequ12 1179  sbequ12r 1180  sbequ12a 1181  sbid 1182  stdpc4 1183  sbf 1184  sb6x 1186  hbs1f 1187  sbequ5 1188  sbequ6 1189  sbt 1190  equsb1 1191  equsb2 1192  sbied 1193  sbie 1194  equs5a 1195  equs5e 1196  equs45f 1198  sb6f 1199  sb5f 1200  aev 1206  ax16 1207  ax17eq 1209  dveeq2 1210  dveeq2ALT 1211  ax11v2 1213  ax11a2 1214  ax11 1217  ax11b 1218  sb3 1220  sb4 1221  sb4b 1222  dfsb2 1223  dfsb3 1224  hbsb2 1225  sbequi 1226  sbequ 1227  drsb2 1228  sbi1 1230  sbequ8 1245  hbsb4 1246  hbsb4t 1247  dvelimf 1248  dvelimdf 1249  sbco 1250  sbidm 1252  sbco2 1253  sbco3 1255  sbcom 1256  sb5rf 1257  sb6rf 1258  sb9i 1261  ax11v 1263  sb56 1264  sb6 1265  sb5 1266  equid1 1267  a4v 1270  a4eiv 1272  equvin 1273  a16g 1274  a16gb 1275  cbval2 1314  cbvex2 1315  cbvald 1318  cbvexd 1319  cbvex4v 1320  cleljust 1326  equsb3lem 1327  equsb3 1328  elsb3 1329  hbs1 1330  hbsb 1331  sbcom2 1332  2sb5 1333  2sb6 1334  sb6a 1335  2sb5rf 1336  2sb6rf 1337  dfsb7 1338  sb7f 1339  sb10f 1340  sbelx 1342  sbel2x 1343  sbal1 1344  sbal 1345  exsb 1348  2exsb 1349  dveeq1 1352  dveeq1ALT 1353  sbal2 1356  ax15 1357  ax17el 1359  ax11eq 1361  ax11el 1362  ax11f 1363  ax11indn 1364  ax11indi 1365  ax11indalem 1366  ax11inda2 1368  ax11inda 1369  a12stdy1 1370  a12stdy3 1372  a12stdy4 1373  a12lem1 1374  a12lem2 1375  a12study 1376  a12studyALT 1377  euf 1382  eubid 1383  eubii 1385  hbeu1 1386  hbeu 1387  sb8eu 1388  eu1 1390  mo 1391  euex 1392  eumo0 1393  eu2 1394  eu3 1395  mo2 1398  mo3 1399  mo4f 1400  mobii 1403  eu5 1407  eu4 1408  immo 1415  moimv 1417  moanim 1425  mopick 1431  2mo 1445  2mos 1446  2eu4 1450  2eu5 1451  2eu6 1452  exists1 1455  exists2 1456  funop 3549  cbvrexf 10410  infi1 10419  ficli 10440  homcard 10498  fgsb2 10521  icmpmon 10659  idmon 10660

Copyright terms: Public domain