Theorem sbceq1a 3788

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  [wsb 2067  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3778

This theorem is referenced by:  sbceq2a  3789  elrabsf  3825  cbvralcsf  3938  reusngf  4676  rexreusng  4683  reuprg0  4706  rmosn  4723  rabsnifsb  4726  euotd  5513  reuop  6292  frpoinsg  6344  wfisgOLD  6355  elfvmptrab1w  7024  elfvmptrab1  7025  ralrnmpt  7097  riotass2  7395  riotass  7396  oprabv  7468  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  ovmpt3rabdm  7664  elovmpt3rab1  7665  tfisg  7842  tfindes  7851  sbcopeq1a  8034  sbcoteq1a  8036  mpoxopoveq  8203  findcard2  9163  findcard2OLD  9283  ac6sfi  9286  indexfi  9359  frinsg  9745  nn0ind-raph  12661  fzrevral  13585  wrdind  14671  wrd2ind  14672  prmind2  16621  elmptrab  23330  isfildlem  23360  2sqreulem4  26954  gropd  28288  grstructd  28289  rspc2daf  31703  opreu2reuALT  31712  ifeqeqx  31769  wrdt2ind  32112  bnj919  33773  bnj976  33783  bnj1468  33852  bnj110  33864  bnj150  33882  bnj151  33883  bnj607  33922  bnj873  33930  bnj849  33931  bnj1388  34039  setinds  34745  dfon2lem1  34750  rdgssun  36254  indexdom  36597  sdclem2  36605  sdclem1  36606  fdc1  36609  riotasv2s  37823  elimhyps  37826  sbccomieg  41521  rexrabdioph  41522  rexfrabdioph  41523  aomclem6  41791  pm13.13a  43156  pm13.13b  43157  pm13.14  43158  tratrb  43287  uzwo4  43730  or2expropbilem2  45733  reuf1odnf  45805  ich2exprop  46129  ichnreuop  46130  ichreuopeq  46131  prproropreud  46167  reupr  46180  reuopreuprim  46184