Theorem wsb 1208

Description: Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff ph").

(Instead of introducing wsb 1208 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 wsbc 1207. This lets us avoid overloading its connectives, thus preventing ambiguity that would complicate some Metamath parsers. Note: To see the proof steps of this syntax proof, type "show proof wsb /all" in the Metamath program.)

Assertion

Ref	Expression
wsb	wff [y / x]ph

Proof of Theorem wsb

Step	Hyp	Ref	Expression
1		wsbc 1207	1 wff [y / x]ph

Syntax hints:  [wsbc 1207

This theorem is referenced by:  sbimi 1210  sbbii 1211  drsb1 1212  sb1 1213  sb2 1214  sbequ1 1215  sbequ2 1216  stdpc7 1217  sbequ12 1218  sbequ12r 1219  sbequ12a 1220  sbid 1221  stdpc4 1222  sbf 1223  sb6x 1225  hbs1f 1226  sbt 1229  equsb1 1230  equsb2 1231  sbied 1232  sbie 1233  sb4a 1236  sb6f 1238  sb5f 1239  sb4e 1240  hbsb2a 1241  hbsb2e 1242  hbsb3 1243  ax16 1246  sb3 1259  sb4 1260  sb4b 1261  dfsb2 1262  dfsb3 1263  hbsb2 1264  sbequi 1265  sbequ 1266  drsb2 1267  sbn 1268  sbi1 1269  sbi2 1270  sbim 1271  sbor 1272  sb19.21 1273  sban 1274  sb3an 1275  sbbi 1276  sblbis 1277  sbrbis 1278  sbrbif 1279  a4sbe 1280  a4sbim 1281  a4sbbi 1282  sbbid 1283  sbequ8 1284  sbf3t 1285  hbsb4 1286  hbsb4t 1287  dvelimf 1288  dvelimdf 1289  sbco 1290  sbid2 1291  sbidm 1292  sbco2 1293  sbco2d 1294  sbco3 1295  sbcom 1296  sb5rf 1297  sb6rf 1298  sb8 1299  sb8e 1300  sb9i 1301  sb9 1302  sb6 1305  sb5 1306  ax16ALT 1309  sbhb 1367  equsb3lem 1368  equsb3 1369  elsb3 1370  hbs1 1371  hbsb 1372  sbcom2 1373  2sb5 1374  2sb6 1375  sb6a 1376  2sb5rf 1377  2sb6rf 1378  dfsb7 1379  sb7f 1380  sb10f 1381  sbelx 1383  sbel2x 1384  sbal1 1385  sbal 1386  sbex 1387  sbalv 1388  exsb 1389  sbal2 1397  sb8eu 1429  cbveu 1430  eu1 1431  mo 1432  euex 1433  eu2 1435  eu3 1436  mo3 1440  mo4f 1441  mopick 1472  2mo 1487  2mos 1488  2eu6 1494  sbc7g 2003  ac6sfilem3 4590  ac6sfi 4591  gapm 11784  indexf 11847

Copyright terms: Public domain