Theorem sbceq1a 3734

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  [wsb 2073  [wsbc 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sbc 3724

This theorem is referenced by:  sbceq2a  3735  elrabsf  3768  cbvralcsf  3873  reusngf  4606  rexreusng  4611  reuprg0  4634  rmosn  4651  rabsnifsb  4654  euotd  5454  reuop  6244  frpoinsg  6294  elfvmptrab1w  6963  elfvmptrab1  6964  ralrnmpt  7037  riotass2  7343  riotass  7344  oprabv  7416  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  ovmpt3rabdm  7615  elovmpt3rab1  7616  tfisg  7794  tfindes  7803  sbcopeq1a  7991  sbcoteq1a  7993  mpoxopoveq  8159  findcard2  9089  ac6sfi  9184  indexfi  9260  setinds  9661  frinsg  9666  nn0ind-raph  12620  fzrevral  13557  wrdind  14675  wrd2ind  14676  prmind2  16645  elmptrab  23810  isfildlem  23840  2sqreulem4  27435  gropd  29118  grstructd  29119  rspc2daf  32553  opreu2reuALT  32564  ifeqeqx  32630  wrdt2ind  33032  bnj919  34950  bnj976  34960  bnj1468  35028  bnj110  35040  bnj150  35058  bnj151  35059  bnj607  35098  bnj873  35106  bnj849  35107  bnj1388  35215  dfon2lem1  36009  rdgssun  37740  indexdom  38101  sdclem2  38109  sdclem1  38110  fdc1  38113  riotasv2s  39450  elimhyps  39453  sbccomieg  43238  rexrabdioph  43239  rexfrabdioph  43240  aomclem6  43504  pm13.13a  44851  pm13.13b  44852  pm13.14  44853  tratrb  44980  uzwo4  45501  or2expropbilem2  47496  reuf1odnf  47570  ich2exprop  47946  ichnreuop  47947  ichreuopeq  47948  prproropreud  47984  reupr  47997  reuopreuprim  48001