Theorem sbceq1a 3131

Description: Equality theorem for class substitution. Class version of sbequ12 1940. (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 1943	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3124	. 2 |- ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3	1, 2	syl5bbr 251	1 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   [wsb 1655   [.wsbc 3121

This theorem is referenced by:  sbceq2a  3132  elrabsf  3159  cbvralcsf  3271  euotd  4417  tfindes  4801  ralrnmpt  5837  sbcopeq1a  6358  mpt2xopoveq  6429  riotass2  6536  riotass  6537  riotasv2s  6555  findcard2  7307  ac6sfi  7310  indexfi  7372  uzindOLD  10320  nn0ind-raph  10326  fzrevral  11086  wrdind  11746  prmind2  13045  elmptrab  17812  isfildlem  17842  ifeqeqx  23954  setinds  25348  dfon2lem1  25353  tfisg  25418  wfisg  25423  frinsg  25459  indexdom  26326  sdclem2  26336  sdclem1  26337  fdc1  26340  sbccomieg  26739  rexrabdioph  26744  rexfrabdioph  26745  aomclem6  27024  pm13.13a  27475  pm13.13b  27476  pm13.14  27477  tratrb  28331  bnj919  28842  bnj976  28854  bnj1468  28923  bnj110  28935  bnj150  28953  bnj151  28954  bnj607  28993  bnj873  29001  bnj849  29002  bnj1388  29108

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-sbc 3122