Theorem sbceq1a 3342

Description: Equality theorem for class substitution. Class version of sbequ12 1961. (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 1965	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3334	. 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 1379   [wsb 1711   [.wsbc 3331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-sbc 3332

This theorem is referenced by:  sbceq2a  3343  elrabsf  3370  cbvralcsf  3467  rabsnifsb  4095  euotd  4748  elfvmptrab1  5968  ralrnmpt  6028  riotass2  6270  riotass  6271  oprabv  6327  elovmpt2rab  6503  elovmpt2rab1  6504  ovmpt3rabdm  6517  elovmpt3rab1  6518  tfindes  6675  sbcopeq1a  6833  mpt2xopoveq  6944  findcard2  7756  ac6sfi  7760  indexfi  7824  uzindOLD  10951  nn0ind-raph  10957  fzrevral  11758  wrdind  12661  wrd2ind  12662  prmind2  14083  elmptrab  20063  isfildlem  20093  ifeqeqx  27093  setinds  28787  dfon2lem1  28792  tfisg  28861  wfisg  28866  frinsg  28902  indexdom  29828  sdclem2  29838  sdclem1  29839  fdc1  29842  sbccomieg  30330  rexrabdioph  30331  rexfrabdioph  30332  aomclem6  30609  pm13.13a  30892  pm13.13b  30893  pm13.14  30894  tratrb  32386  bnj919  32904  bnj976  32915  bnj1468  32983  bnj110  32995  bnj150  33013  bnj151  33014  bnj607  33053  bnj873  33061  bnj849  33062  bnj1388  33168  riotasv2s  33761