Theorem sbceq1a 3757

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

Assertion

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

Proof of Theorem sbceq1a

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099  [wsbc 3746

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3747

This theorem is used by:  sbceq2a  3758  elrabsf  3791  cbvralcsf  3896  reusngf  4642  rexreusng  4647  reuprg0  4670  rmosn  4687  rabsnifsb  4690  euotd  5498  reuop  6298  frpoinsg  6348  elfvmptrab1w  7021  elfvmptrab1  7022  ralrnmpt  7095  riotass2  7403  riotass  7404  oprabv  7476  elovmporab  7662  elovmporab1w  7663  elovmporab1  7664  ovmpt3rabdm  7675  elovmpt3rab1  7676  tfisg  7852  tfindes  7861  sbcopeq1a  8048  sbcoteq1a  8050  mpoxopoveq  8217  findcard2  9152  ac6sfi  9247  indexfi  9320  setinds  9721  frinsg  9726  nn0ind-raph  12707  fzrevral  13652  wrdind  14776  wrd2ind  14777  prmind2  16760  elmptrab  24013  isfildlem  24043  2sqreulem4  27647  gropd  29410  grstructd  29411  rspc2daf  32842  opreu2reuALT  32852  ifeqeqx  32917  wrdt2ind  33298  bnj919  35180  bnj976  35190  bnj1468  35258  bnj110  35270  bnj150  35288  bnj151  35289  bnj607  35328  bnj873  35336  bnj849  35337  bnj1388  35445  dfon2lem1  36286  rdgssun  38057  indexdom  38418  sdclem2  38426  sdclem1  38427  fdc1  38430  riotasv2s  39765  elimhyps  39768  sbccomieg  43553  rexrabdioph  43554  rexfrabdioph  43555  aomclem6  43819  pm13.13a  45150  pm13.13b  45151  pm13.14  45152  tratrb  45278  uzwo4  45806  or2expropbilem2  47803  reuf1odnf  47877  ich2exprop  48253  ichnreuop  48254  ichreuopeq  48255  prproropreud  48291  reupr  48304  reuopreuprim  48308