Theorem sbceq1a 3799

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2064  [wsbc 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789

This theorem is referenced by:  sbceq2a  3800  elrabsf  3834  cbvralcsf  3941  reusngf  4674  rexreusng  4679  reuprg0  4702  rmosn  4719  rabsnifsb  4722  euotd  5518  reuop  6313  frpoinsg  6364  wfisgOLD  6375  elfvmptrab1w  7043  elfvmptrab1  7044  ralrnmpt  7116  riotass2  7418  riotass  7419  oprabv  7493  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ovmpt3rabdm  7692  elovmpt3rab1  7693  tfisg  7875  tfindes  7884  sbcopeq1a  8074  sbcoteq1a  8076  mpoxopoveq  8244  findcard2  9204  ac6sfi  9320  indexfi  9400  frinsg  9791  nn0ind-raph  12718  fzrevral  13652  wrdind  14760  wrd2ind  14761  prmind2  16722  elmptrab  23835  isfildlem  23865  2sqreulem4  27498  gropd  29048  grstructd  29049  rspc2daf  32485  opreu2reuALT  32496  ifeqeqx  32555  wrdt2ind  32938  bnj919  34781  bnj976  34791  bnj1468  34860  bnj110  34872  bnj150  34890  bnj151  34891  bnj607  34930  bnj873  34938  bnj849  34939  bnj1388  35047  setinds  35779  dfon2lem1  35784  rdgssun  37379  indexdom  37741  sdclem2  37749  sdclem1  37750  fdc1  37753  riotasv2s  38959  elimhyps  38962  sbccomieg  42804  rexrabdioph  42805  rexfrabdioph  42806  aomclem6  43071  pm13.13a  44426  pm13.13b  44427  pm13.14  44428  tratrb  44556  uzwo4  45058  or2expropbilem2  47045  reuf1odnf  47119  ich2exprop  47458  ichnreuop  47459  ichreuopeq  47460  prproropreud  47496  reupr  47509  reuopreuprim  47513