Theorem wsb 1173

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

(Instead of introducing wsb 1173 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 1172. 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]φ

Proof of Theorem wsb

Step	Hyp	Ref	Expression
1		wsbc 1172	1 wff [y / x]φ

Syntax hints:  [wsbc 1172

This theorem is referenced by:  sbimi 1175  sbbii 1176  drsb1 1177  sb1 1178  sb2 1179  sbequ1 1180  sbequ2 1181  stdpc7 1182  sbequ12 1183  sbequ12r 1184  sbequ12a 1185  sbid 1186  stdpc4 1187  sbf 1188  sb6x 1190  hbs1f 1191  sbt 1194  equsb1 1195  equsb2 1196  sbied 1197  sbie 1198  sb6f 1203  sb5f 1204  ax16 1211  sb3 1224  sb4 1225  sb4b 1226  dfsb2 1227  dfsb3 1228  hbsb2 1229  sbequi 1230  sbequ 1231  drsb2 1232  sbn 1233  sbi1 1234  sbi2 1235  sbim 1236  sbor 1237  sb19.21 1238  sban 1239  sb3an 1240  sbbi 1241  sblbis 1242  sbrbis 1243  sbrbif 1244  a4sbe 1245  a4sbim 1246  a4sbbi 1247  sbbid 1248  sbequ8 1249  hbsb4 1250  hbsb4t 1251  dvelimf 1252  dvelimdf 1253  sbco 1254  sbid2 1255  sbidm 1256  sbco2 1257  sbco2d 1258  sbco3 1259  sbcom 1260  sb5rf 1261  sb6rf 1262  sb8 1263  sb8e 1264  sb9i 1265  sb9 1266  sb6 1269  sb5 1270  equsb3lem 1331  equsb3 1332  elsb3 1333  hbs1 1334  hbsb 1335  sbcom2 1336  2sb5 1337  2sb6 1338  sb6a 1339  2sb5rf 1340  2sb6rf 1341  dfsb7 1342  sb7f 1343  sb10f 1344  sbelx 1346  sbel2x 1347  sbal1 1348  sbal 1349  sbex 1350  sbalv 1351  exsb 1352  sbal2 1360  sb8eu 1392  cbveu 1393  eu1 1394  mo 1395  euex 1396  eu2 1398  eu3 1399  mo3 1403  mo4f 1404  mopick 1435  2mo 1450  2mos 1451  2eu6 1457

Copyright terms: Public domain