Theorem sbequ12 1218

Description: An equality theorem for substitution.

Assertion

Ref	Expression
sbequ12	|- (x = y -> (ph <-> [y / x]ph))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 1215	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1216	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 519	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992  [wsbc 1207

This theorem is referenced by:  sbequ12r 1219  sbequ12a 1220  sbid 1221  ax16 1246  sbco 1290  sbidm 1292  sbco2 1293  sbcom 1296  ax16ALT 1309  sbcom2 1373  sb6a 1376  sbal1 1385  mopick 1472  2mo 1487  2eu6 1494  clelab 1624  sbab 1626  moi2 1970  moi 1971  reu2 1976  reu3 1977  sbhypf 1985  sbralie 1986  elrabsf 2011  cbvralsv 2015  cbvrexsv 2016  csbabg 2095  iunrab 2664  cbvopab1s 2749  opabid 2887  opelopabsb 2892  opelopabf 2899  tfis 3208  tfinds 3212  tfindes 3215  findes 3248  ralxpf 3303  abrexex2 3985  ac6sfi 4591  uzind4s 6579  cau3ii 7117

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 1009

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209

Copyright terms: Public domain