Theorem sbceq1a 3747

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

Assertion

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

Proof of Theorem sbceq1a

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

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

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 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3737

This theorem is referenced by:  sbceq2a  3748  elrabsf  3782  cbvralcsf  3887  reusngf  4622  rexreusng  4627  reuprg0  4650  rmosn  4667  rabsnifsb  4670  euotd  5448  reuop  6235  frpoinsg  6285  elfvmptrab1w  6951  elfvmptrab1  6952  ralrnmpt  7024  riotass2  7328  riotass  7329  oprabv  7401  elovmporab  7587  elovmporab1w  7588  elovmporab1  7589  ovmpt3rabdm  7600  elovmpt3rab1  7601  tfisg  7779  tfindes  7788  sbcopeq1a  7976  sbcoteq1a  7978  mpoxopoveq  8144  findcard2  9069  ac6sfi  9163  indexfi  9239  setinds  9634  frinsg  9639  nn0ind-raph  12568  fzrevral  13507  wrdind  14624  wrd2ind  14625  prmind2  16591  elmptrab  23737  isfildlem  23767  2sqreulem4  27387  gropd  29004  grstructd  29005  rspc2daf  32437  opreu2reuALT  32448  ifeqeqx  32514  wrdt2ind  32926  bnj919  34771  bnj976  34781  bnj1468  34850  bnj110  34862  bnj150  34880  bnj151  34881  bnj607  34920  bnj873  34928  bnj849  34929  bnj1388  35037  dfon2lem1  35817  rdgssun  37412  indexdom  37774  sdclem2  37782  sdclem1  37783  fdc1  37786  riotasv2s  38997  elimhyps  39000  sbccomieg  42826  rexrabdioph  42827  rexfrabdioph  42828  aomclem6  43092  pm13.13a  44440  pm13.13b  44441  pm13.14  44442  tratrb  44569  uzwo4  45090  or2expropbilem2  47064  reuf1odnf  47138  ich2exprop  47502  ichnreuop  47503  ichreuopeq  47504  prproropreud  47540  reupr  47553  reuopreuprim  47557