Theorem sbceq1a 3789

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

Assertion

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

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2248	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3781	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 285	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  [wsb 2068  [wsbc 3778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779

This theorem is referenced by:  sbceq2a  3790  elrabsf  3826  cbvralcsf  3939  reusngf  4677  rexreusng  4684  reuprg0  4707  rmosn  4724  rabsnifsb  4727  euotd  5514  reuop  6293  frpoinsg  6345  wfisgOLD  6356  elfvmptrab1w  7025  elfvmptrab1  7026  ralrnmpt  7098  riotass2  7396  riotass  7397  oprabv  7469  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  ovmpt3rabdm  7665  elovmpt3rab1  7666  tfisg  7843  tfindes  7852  sbcopeq1a  8035  sbcoteq1a  8037  mpoxopoveq  8204  findcard2  9164  findcard2OLD  9284  ac6sfi  9287  indexfi  9360  frinsg  9746  nn0ind-raph  12662  fzrevral  13586  wrdind  14672  wrd2ind  14673  prmind2  16622  elmptrab  23331  isfildlem  23361  2sqreulem4  26957  gropd  28291  grstructd  28292  rspc2daf  31708  opreu2reuALT  31717  ifeqeqx  31774  wrdt2ind  32117  bnj919  33778  bnj976  33788  bnj1468  33857  bnj110  33869  bnj150  33887  bnj151  33888  bnj607  33927  bnj873  33935  bnj849  33936  bnj1388  34044  setinds  34750  dfon2lem1  34755  rdgssun  36259  indexdom  36602  sdclem2  36610  sdclem1  36611  fdc1  36614  riotasv2s  37828  elimhyps  37831  sbccomieg  41531  rexrabdioph  41532  rexfrabdioph  41533  aomclem6  41801  pm13.13a  43166  pm13.13b  43167  pm13.14  43168  tratrb  43297  uzwo4  43740  or2expropbilem2  45743  reuf1odnf  45815  ich2exprop  46139  ichnreuop  46140  ichreuopeq  46141  prproropreud  46177  reupr  46190  reuopreuprim  46194