Theorem wsb 1171

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 1171 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 1170. 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 1170	1 wff [y / x]ph

Syntax hints:  [wsbc 1170

This theorem is referenced by:  sbimi 1173  sbbii 1174  drsb1 1175  sb1 1176  sb2 1177  sbequ1 1178  sbequ2 1179  stdpc7 1180  sbequ12 1181  sbequ12r 1182  sbequ12a 1183  sbid 1184  stdpc4 1185  sbf 1186  sb6x 1188  hbs1f 1189  sbt 1192  equsb1 1193  equsb2 1194  sbied 1195  sbie 1196  sb6f 1201  sb5f 1202  ax16 1209  sb3 1222  sb4 1223  sb4b 1224  dfsb2 1225  dfsb3 1226  hbsb2 1227  sbequi 1228  sbequ 1229  drsb2 1230  sbn 1231  sbi1 1232  sbi2 1233  sbim 1234  sbor 1235  sb19.21 1236  sban 1237  sb3an 1238  sbbi 1239  sblbis 1240  sbrbis 1241  sbrbif 1242  a4sbe 1243  a4sbim 1244  a4sbbi 1245  sbbid 1246  sbequ8 1247  hbsb4 1248  hbsb4t 1249  dvelimf 1250  dvelimdf 1251  sbco 1252  sbid2 1253  sbidm 1254  sbco2 1255  sbco2d 1256  sbco3 1257  sbcom 1258  sb5rf 1259  sb6rf 1260  sb8 1261  sb8e 1262  sb9i 1263  sb9 1264  sb6 1267  sb5 1268  equsb3lem 1329  equsb3 1330  elsb3 1331  hbs1 1332  hbsb 1333  sbcom2 1334  2sb5 1335  2sb6 1336  sb6a 1337  2sb5rf 1338  2sb6rf 1339  dfsb7 1340  sb7f 1341  sb10f 1342  sbelx 1344  sbel2x 1345  sbal1 1346  sbal 1347  sbex 1348  sbalv 1349  exsb 1350  sbal2 1358  sb8eu 1390  cbveu 1391  eu1 1392  mo 1393  euex 1394  eu2 1396  eu3 1397  mo3 1401  mo4f 1402  mopick 1433  2mo 1447  2mos 1448  2eu6 1454

Copyright terms: Public domain