Theorem sbequ12 1545

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 1542	. 2 |- (x = y -> (ph -> [y / x]ph))
2		sbequ2 1543	. 2 |- (x = y -> ([y / x]ph -> ph))
3	1, 2	impbid 574	1 |- (x = y -> (ph <-> [y / x]ph))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  [wsbc 1534

This theorem is referenced by:  sbequ12r 1546  sbequ12rOLD 1547  sbequ12a 1548  sbid 1549  ax16 1579  sbco 1625  sbidmOLD 1628  sbco2 1629  sbcom 1632  ax16ALT 1648  sbcom2 1724  sb6a 1727  sbal1 1737  mopick 1833  2mo 1851  2eu6 1858  clelab 2013  sbab 2015  cbvralf 2276  cbvrexf 2277  cbvrab 2421  moi2 2435  moi 2436  reu2 2442  reu6 2443  sbhypf 2452  sbralie 2453  elrabsf 2486  cbvralsv 2490  cbvralsvOLD 2491  cbvrexsv 2492  cbvrexsvOLD 2493  sbcralg 2531  sbcrexg 2533  csbabgOLD 2589  iunrab 3299  iinab 3317  cbvopab1 3405  cbvopab1s 3406  opabidOLD 3558  opelopabsbOLD 3565  opelopabf 3572  tfis 3938  tfinds 3942  tfindsOLD 3943  tfindes 3946  findes 3983  ralxpf 4043  abrexex2 4847  cbvmpt 5011  ac6sfi 5509  uzind4s 7621  cau3ii 8166  bnj47 12417  bnj54OLD 12429  bnj971 12860  bnj1216 12989  bnj1306 13049  bnj1310 13050  bnj1366 13091  bnj1468 13145  bnj1492 13161  bnj149 13241  bnj607 13304  bnj873 13317  bnj1390 13513  setinds 13844  dfon2lem1 13849  tfisg 13912  wfisg 13917  frinsg 13941  findcard2 15745  fdc1 15813  pm13.193 16375  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  cbviotaf 16432

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain