Theorem sbceq1a 3749

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

Assertion

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

Proof of Theorem sbceq1a

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  [wsb 2098  [wsbc 3738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbceq2a  3750  elrabsf  3783  cbvralcsf  3888  reusngf  4631  rexreusng  4636  reuprg0  4659  rmosn  4676  rabsnifsb  4679  euotd  5485  reuop  6296  frpoinsg  6346  elfvmptrab1w  7022  elfvmptrab1  7023  ralrnmpt  7097  riotass2  7408  riotass  7409  oprabv  7481  elovmporab  7668  elovmporab1w  7669  elovmporab1  7670  ovmpt3rabdm  7681  elovmpt3rab1  7682  tfisg  7866  tfindes  7875  sbcopeq1a  8061  sbcoteq1a  8063  mpoxopoveq  8240  findcard2  9184  ac6sfi  9279  indexfi  9353  setinds  9754  frinsg  9759  nn0ind-raph  12803  fzrevral  13750  wrdind  14876  wrd2ind  14877  prmind2  16866  elmptrab  24152  isfildlem  24182  2sqreulem4  27787  gropd  29615  grstructd  29616  rspc2daf  33111  opreu2reuALT  33121  ifeqeqx  33186  wrdt2ind  33563  bnj919  35445  bnj976  35455  bnj1468  35523  bnj110  35535  bnj150  35553  bnj151  35554  bnj607  35593  bnj873  35601  bnj849  35602  bnj1388  35710  rdgssun  38395  indexdom  38762  sdclem2  38770  sdclem1  38771  fdc1  38774  riotasv2s  40109  elimhyps  40112  sbccomieg  43894  rexrabdioph  43895  rexfrabdioph  43896  aomclem6  44155  pm13.13a  45485  pm13.13b  45486  pm13.14  45487  tratrb  45613  uzwo4  46164  or2expropbilem2  48197  reuf1odnf  48271  ich2exprop  48647  ichnreuop  48648  ichreuopeq  48649  prproropreud  48685  reupr  48698  reuopreuprim  48702