Theorem sbceq1a 3753

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

Assertion

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

Proof of Theorem sbceq1a

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  sbceq2a  3754  elrabsf  3787  cbvralcsf  3893  reusngf  4636  rexreusng  4641  reuprg0  4664  rmosn  4682  rabsnifsb  4685  euotd  5493  reuop  6322  frpoinsg  6372  elfvmptrab1w  7052  elfvmptrab1  7053  ralrnmpt  7128  riotass2  7438  riotass  7439  oprabv  7511  elovmporab  7699  elovmporab1w  7700  elovmporab1  7701  ovmpt3rabdm  7712  elovmpt3rab1  7713  tfisg  7899  tfindes  7908  sbcopeq1a  8095  sbcoteq1a  8097  mpoxopoveq  8274  findcard2  9218  ac6sfi  9313  indexfi  9387  setinds  9787  frinsg  9792  nn0ind-raph  12839  fzrevral  13786  wrdind  14913  wrd2ind  14914  prmind2  16904  elmptrab  24201  isfildlem  24231  2sqreulem4  27838  gropd  29666  grstructd  29667  rspc2daf  33162  opreu2reuALT  33172  ifeqeqx  33236  wrdt2ind  33612  bnj919  35509  bnj976  35519  bnj1468  35587  bnj110  35599  bnj150  35617  bnj151  35618  bnj607  35657  bnj873  35665  bnj849  35666  bnj1388  35774  rdgssun  38569  indexdom  38936  sdclem2  38942  sdclem1  38943  fdc1  38946  riotasv2s  40281  elimhyps  40284  sbccomieg  44066  rexrabdioph  44067  rexfrabdioph  44068  aomclem6  44327  pm13.13a  45652  pm13.13b  45653  pm13.14  45654  tratrb  45779  uzwo4  46344  or2expropbilem2  48376  reuf1odnf  48451  ich2exprop  48826  ichnreuop  48827  ichreuopeq  48828  prproropreud  48864  reupr  48877  reuopreuprim  48881