Theorem sbceq1a 3192

Description: Equality theorem for class substitution. Class version of sbequ12 1936. (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 1940	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3184	. 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 1369   [wsb 1700   [.wsbc 3181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-sbc 3182

This theorem is referenced by:  sbceq2a  3193  elrabsf  3220  cbvralcsf  3314  rabsnifsb  3938  euotd  4587  ralrnmpt  5847  riotass2  6074  riotass  6075  tfindes  6468  sbcopeq1a  6621  mpt2xopoveq  6731  findcard2  7544  ac6sfi  7548  indexfi  7611  uzindOLD  10728  nn0ind-raph  10734  fzrevral  11536  wrdind  12363  wrd2ind  12364  prmind2  13766  elmptrab  19380  isfildlem  19410  ifeqeqx  25870  setinds  27560  dfon2lem1  27565  tfisg  27634  wfisg  27639  frinsg  27675  indexdom  28599  sdclem2  28609  sdclem1  28610  fdc1  28613  sbccomieg  29102  rexrabdioph  29103  rexfrabdioph  29104  aomclem6  29383  pm13.13a  29632  pm13.13b  29633  pm13.14  29634  elfvmptrab1  30125  oprabv  30128  elovmpt2rab  30129  elovmpt2rab1  30130  ovmpt3rabdm  30133  elovmpt3rab1  30134  tratrb  31171  bnj919  31689  bnj976  31700  bnj1468  31768  bnj110  31780  bnj150  31798  bnj151  31799  bnj607  31838  bnj873  31846  bnj849  31847  bnj1388  31953  riotasv2s  32502