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  28322  grstructd  28323  rspc2daf  31739  opreu2reuALT  31748  ifeqeqx  31805  wrdt2ind  32148  bnj919  33809  bnj976  33819  bnj1468  33888  bnj110  33900  bnj150  33918  bnj151  33919  bnj607  33958  bnj873  33966  bnj849  33967  bnj1388  34075  setinds  34781  dfon2lem1  34786  rdgssun  36307  indexdom  36650  sdclem2  36658  sdclem1  36659  fdc1  36662  riotasv2s  37876  elimhyps  37879  sbccomieg  41579  rexrabdioph  41580  rexfrabdioph  41581  aomclem6  41849  pm13.13a  43214  pm13.13b  43215  pm13.14  43216  tratrb  43345  uzwo4  43788  or2expropbilem2  45791  reuf1odnf  45863  ich2exprop  46187  ichnreuop  46188  ichreuopeq  46189  prproropreud  46225  reupr  46238  reuopreuprim  46242