Theorem sbceq1a 3335

Description: Equality theorem for class substitution. Class version of sbequ12 1997. (Contributed by NM, 26-Sep-2003.)

Assertion

Ref	Expression
sbceq1a	|- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2001	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3327	. 2 |- ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3	1, 2	syl5bbr 259	1 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1398   [wsb 1744   [.wsbc 3324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3325

This theorem is referenced by:  sbceq2a  3336  elrabsf  3363  cbvralcsf  3452  rabsnifsb  4084  euotd  4737  elfvmptrab1  5952  ralrnmpt  6016  riotass2  6258  riotass  6259  oprabv  6318  elovmpt2rab  6494  elovmpt2rab1  6495  ovmpt3rabdm  6508  elovmpt3rab1  6509  tfindes  6670  sbcopeq1a  6825  mpt2xopoveq  6939  findcard2  7752  ac6sfi  7756  indexfi  7820  uzindOLD  10953  nn0ind-raph  10960  fzrevral  11767  wrdind  12696  wrd2ind  12697  prmind2  14315  elmptrab  20497  isfildlem  20527  ifeqeqx  27628  setinds  29453  dfon2lem1  29458  tfisg  29527  wfisg  29532  frinsg  29568  indexdom  30468  sdclem2  30478  sdclem1  30479  fdc1  30482  sbccomieg  30969  rexrabdioph  30970  rexfrabdioph  30971  aomclem6  31247  pm13.13a  31558  pm13.13b  31559  pm13.14  31560  tratrb  33716  bnj919  34245  bnj976  34256  bnj1468  34324  bnj110  34336  bnj150  34354  bnj151  34355  bnj607  34394  bnj873  34402  bnj849  34403  bnj1388  34509  riotasv2s  35105