Theorem sbceq1a 3753

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  sbceq2a  3754  elrabsf  3788  cbvralcsf  3893  reusngf  4633  rexreusng  4638  reuprg0  4661  rmosn  4678  rabsnifsb  4681  euotd  5469  reuop  6259  frpoinsg  6309  elfvmptrab1w  6977  elfvmptrab1  6978  ralrnmpt  7050  riotass2  7355  riotass  7356  oprabv  7428  elovmporab  7614  elovmporab1w  7615  elovmporab1  7616  ovmpt3rabdm  7627  elovmpt3rab1  7628  tfisg  7806  tfindes  7815  sbcopeq1a  8003  sbcoteq1a  8005  mpoxopoveq  8171  findcard2  9101  ac6sfi  9196  indexfi  9272  setinds  9670  frinsg  9675  nn0ind-raph  12604  fzrevral  13540  wrdind  14657  wrd2ind  14658  prmind2  16624  elmptrab  23783  isfildlem  23813  2sqreulem4  27433  gropd  29116  grstructd  29117  rspc2daf  32551  opreu2reuALT  32562  ifeqeqx  32628  wrdt2ind  33045  bnj919  34943  bnj976  34953  bnj1468  35021  bnj110  35033  bnj150  35051  bnj151  35052  bnj607  35091  bnj873  35099  bnj849  35100  bnj1388  35208  dfon2lem1  35994  rdgssun  37630  indexdom  37982  sdclem2  37990  sdclem1  37991  fdc1  37994  riotasv2s  39331  elimhyps  39334  sbccomieg  43147  rexrabdioph  43148  rexfrabdioph  43149  aomclem6  43413  pm13.13a  44760  pm13.13b  44761  pm13.14  44762  tratrb  44889  uzwo4  45410  or2expropbilem2  47390  reuf1odnf  47464  ich2exprop  47828  ichnreuop  47829  ichreuopeq  47830  prproropreud  47866  reupr  47879  reuopreuprim  47883