Theorem sbceq1a 3785

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

Assertion

Ref	Expression
sbceq1a	⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2257	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3777	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	syl5bbr 287	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  [wsb 2069  [wsbc 3774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-sbc 3775

This theorem is referenced by:  sbceq2a  3786  elrabsf  3818  cbvralcsf  3927  vtocl2dOLD  3933  reusngf  4614  rexreusng  4619  reuprg0  4640  rmosn  4657  rabsnifsb  4660  euotd  5405  reuop  6146  wfisg  6185  elfvmptrab1w  6796  elfvmptrab1  6797  ralrnmpt  6864  riotass2  7146  riotass  7147  oprabv  7216  elovmporab  7393  elovmporab1w  7394  elovmporab1  7395  ovmpt3rabdm  7406  elovmpt3rab1  7407  tfindes  7579  sbcopeq1a  7750  mpoxopoveq  7887  findcard2  8760  ac6sfi  8764  indexfi  8834  nn0ind-raph  12085  fzrevral  12995  wrdind  14086  wrd2ind  14087  prmind2  16031  elmptrab  22437  isfildlem  22467  2sqreulem4  26032  gropd  26818  grstructd  26819  rspc2daf  30233  opreu2reuALT  30242  ifeqeqx  30299  wrdt2ind  30629  bnj919  32040  bnj976  32051  bnj1468  32120  bnj110  32132  bnj150  32150  bnj151  32151  bnj607  32190  bnj873  32198  bnj849  32199  bnj1388  32307  setinds  33025  dfon2lem1  33030  tfisg  33057  frpoinsg  33083  frinsg  33089  rdgssun  34661  indexdom  35011  sdclem2  35019  sdclem1  35020  fdc1  35023  riotasv2s  36096  elimhyps  36099  sbccomieg  39397  rexrabdioph  39398  rexfrabdioph  39399  aomclem6  39666  pm13.13a  40746  pm13.13b  40747  pm13.14  40748  tratrb  40877  uzwo4  41322  or2expropbilem2  43275  reuf1odnf  43313  ich2exprop  43640  ichnreuop  43641  ichreuopeq  43642  prproropreud  43678  reupr  43691  reuopreuprim  43695