Theorem sbceq1a 3722

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2068  [wsbc 3711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sbc 3712

This theorem is referenced by:  sbceq2a  3723  elrabsf  3759  cbvralcsf  3873  reusngf  4605  rexreusng  4612  reuprg0  4635  rmosn  4652  rabsnifsb  4655  euotd  5421  reuop  6185  frpoinsg  6231  wfisgOLD  6242  elfvmptrab1w  6883  elfvmptrab1  6884  ralrnmpt  6954  riotass2  7243  riotass  7244  oprabv  7313  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  ovmpt3rabdm  7506  elovmpt3rab1  7507  tfindes  7684  sbcopeq1a  7863  mpoxopoveq  8006  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  indexfi  9057  frinsg  9440  nn0ind-raph  12350  fzrevral  13270  wrdind  14363  wrd2ind  14364  prmind2  16318  elmptrab  22886  isfildlem  22916  2sqreulem4  26507  gropd  27304  grstructd  27305  rspc2daf  30717  opreu2reuALT  30726  ifeqeqx  30786  wrdt2ind  31127  bnj919  32647  bnj976  32657  bnj1468  32726  bnj110  32738  bnj150  32756  bnj151  32757  bnj607  32796  bnj873  32804  bnj849  32805  bnj1388  32913  sbcoteq1a  33590  setinds  33660  dfon2lem1  33665  tfisg  33692  rdgssun  35476  indexdom  35819  sdclem2  35827  sdclem1  35828  fdc1  35831  riotasv2s  36899  elimhyps  36902  sbccomieg  40531  rexrabdioph  40532  rexfrabdioph  40533  aomclem6  40800  pm13.13a  41914  pm13.13b  41915  pm13.14  41916  tratrb  42045  uzwo4  42490  or2expropbilem2  44414  reuf1odnf  44486  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  prproropreud  44849  reupr  44862  reuopreuprim  44866