Theorem sbceq1a 3748

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

Assertion

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

Proof of Theorem sbceq1a

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

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

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 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738

This theorem is referenced by:  sbceq2a  3749  elrabsf  3783  cbvralcsf  3888  reusngf  4628  rexreusng  4633  reuprg0  4656  rmosn  4673  rabsnifsb  4676  euotd  5458  reuop  6248  frpoinsg  6298  elfvmptrab1w  6965  elfvmptrab1  6966  ralrnmpt  7038  riotass2  7342  riotass  7343  oprabv  7415  elovmporab  7601  elovmporab1w  7602  elovmporab1  7603  ovmpt3rabdm  7614  elovmpt3rab1  7615  tfisg  7793  tfindes  7802  sbcopeq1a  7990  sbcoteq1a  7992  mpoxopoveq  8158  findcard2  9085  ac6sfi  9179  indexfi  9255  setinds  9650  frinsg  9655  nn0ind-raph  12583  fzrevral  13519  wrdind  14636  wrd2ind  14637  prmind2  16603  elmptrab  23762  isfildlem  23792  2sqreulem4  27412  gropd  29030  grstructd  29031  rspc2daf  32466  opreu2reuALT  32477  ifeqeqx  32543  wrdt2ind  32963  bnj919  34851  bnj976  34861  bnj1468  34930  bnj110  34942  bnj150  34960  bnj151  34961  bnj607  35000  bnj873  35008  bnj849  35009  bnj1388  35117  dfon2lem1  35897  rdgssun  37495  indexdom  37847  sdclem2  37855  sdclem1  37856  fdc1  37859  riotasv2s  39130  elimhyps  39133  sbccomieg  42950  rexrabdioph  42951  rexfrabdioph  42952  aomclem6  43216  pm13.13a  44564  pm13.13b  44565  pm13.14  44566  tratrb  44693  uzwo4  45214  or2expropbilem2  47195  reuf1odnf  47269  ich2exprop  47633  ichnreuop  47634  ichreuopeq  47635  prproropreud  47671  reupr  47684  reuopreuprim  47688