Theorem wsb 1167

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 1167 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 1166. This lets us avoid overloading its connectives, thus preventing ambiguity that causes problems in certain 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 1166	1 wff [y / x]ph

Syntax hints:  [wsbc 1166

This theorem is referenced by:  sbimi 1169  sbbii 1170  drsb1 1171  sb1 1172  sb2 1173  sbequ1 1174  sbequ2 1175  stdpc7 1176  sbequ12 1177  sbequ12r 1178  sbequ12a 1179  sbid 1180  stdpc4 1181  sbf 1182  sb6x 1184  hbs1f 1185  sbt 1188  equsb1 1189  equsb2 1190  sbied 1191  sbie 1192  sb6f 1197  sb5f 1198  ax16 1205  sb3 1217  sb4 1218  sb4b 1219  dfsb2 1220  dfsb3 1221  hbsb2 1222  sbequi 1223  sbequ 1224  drsb2 1225  sbn 1226  sbi1 1227  sbi2 1228  sbim 1229  sbor 1230  sb19.21 1231  sban 1232  sb3an 1233  sbbi 1234  sblbis 1235  sbrbis 1236  sbrbif 1237  a4sbe 1238  a4sbim 1239  a4sbbi 1240  sbbid 1241  sbequ8 1242  hbsb4 1243  hbsb4t 1244  dvelimf 1245  dvelimdf 1246  sbco 1247  sbid2 1248  sbidm 1249  sbco2 1250  sbco2d 1251  sbco3 1252  sbcom 1253  sb5rf 1254  sb6rf 1255  sb8 1256  sb8e 1257  sb9i 1258  sb9 1259  sb6 1262  sb5 1263  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  sbex 1343  sbalv 1344  exsb 1345  sbal2 1351  sb8eu 1383  cbveu 1384  eu1 1385  mo 1386  euex 1387  eu2 1389  eu3 1390  mo3 1394  mo4f 1395  mopick 1426  2mo 1440  2mos 1441  2eu6 1447

Copyright terms: Public domain