Theorem sbceq1a 3727

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 3719	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 285	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2067  [wsbc 3716

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbceq2a  3728  elrabsf  3764  cbvralcsf  3877  reusngf  4608  rexreusng  4615  reuprg0  4638  rmosn  4655  rabsnifsb  4658  euotd  5427  reuop  6196  frpoinsg  6246  wfisgOLD  6257  elfvmptrab1w  6901  elfvmptrab1  6902  ralrnmpt  6972  riotass2  7263  riotass  7264  oprabv  7335  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  ovmpt3rabdm  7528  elovmpt3rab1  7529  tfindes  7709  sbcopeq1a  7890  mpoxopoveq  8035  findcard2  8947  findcard2OLD  9056  ac6sfi  9058  indexfi  9127  frinsg  9509  nn0ind-raph  12420  fzrevral  13341  wrdind  14435  wrd2ind  14436  prmind2  16390  elmptrab  22978  isfildlem  23008  2sqreulem4  26602  gropd  27401  grstructd  27402  rspc2daf  30816  opreu2reuALT  30825  ifeqeqx  30885  wrdt2ind  31225  bnj919  32747  bnj976  32757  bnj1468  32826  bnj110  32838  bnj150  32856  bnj151  32857  bnj607  32896  bnj873  32904  bnj849  32905  bnj1388  33013  sbcoteq1a  33687  setinds  33754  dfon2lem1  33759  tfisg  33786  rdgssun  35549  indexdom  35892  sdclem2  35900  sdclem1  35901  fdc1  35904  riotasv2s  36972  elimhyps  36975  sbccomieg  40615  rexrabdioph  40616  rexfrabdioph  40617  aomclem6  40884  pm13.13a  42025  pm13.13b  42026  pm13.14  42027  tratrb  42156  uzwo4  42601  or2expropbilem2  44527  reuf1odnf  44599  ich2exprop  44923  ichnreuop  44924  ichreuopeq  44925  prproropreud  44961  reupr  44974  reuopreuprim  44978