Theorem sbceq1a 3751

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067  [wsbc 3740

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  sbceq2a  3752  elrabsf  3786  cbvralcsf  3891  reusngf  4631  rexreusng  4636  reuprg0  4659  rmosn  4676  rabsnifsb  4679  euotd  5461  reuop  6251  frpoinsg  6301  elfvmptrab1w  6968  elfvmptrab1  6969  ralrnmpt  7041  riotass2  7345  riotass  7346  oprabv  7418  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ovmpt3rabdm  7617  elovmpt3rab1  7618  tfisg  7796  tfindes  7805  sbcopeq1a  7993  sbcoteq1a  7995  mpoxopoveq  8161  findcard2  9089  ac6sfi  9184  indexfi  9260  setinds  9658  frinsg  9663  nn0ind-raph  12592  fzrevral  13528  wrdind  14645  wrd2ind  14646  prmind2  16612  elmptrab  23771  isfildlem  23801  2sqreulem4  27421  gropd  29104  grstructd  29105  rspc2daf  32540  opreu2reuALT  32551  ifeqeqx  32617  wrdt2ind  33035  bnj919  34923  bnj976  34933  bnj1468  35002  bnj110  35014  bnj150  35032  bnj151  35033  bnj607  35072  bnj873  35080  bnj849  35081  bnj1388  35189  dfon2lem1  35975  rdgssun  37583  indexdom  37935  sdclem2  37943  sdclem1  37944  fdc1  37947  riotasv2s  39218  elimhyps  39221  sbccomieg  43035  rexrabdioph  43036  rexfrabdioph  43037  aomclem6  43301  pm13.13a  44648  pm13.13b  44649  pm13.14  44650  tratrb  44777  uzwo4  45298  or2expropbilem2  47279  reuf1odnf  47353  ich2exprop  47717  ichnreuop  47718  ichreuopeq  47719  prproropreud  47755  reupr  47768  reuopreuprim  47772