Theorem sbceq1a 3782

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

Assertion

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

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2253	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3774	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	syl5bbr 287	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  [wsb 2065  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  sbceq2a  3783  elrabsf  3815  cbvralcsf  3924  vtocl2dOLD  3930  reusngf  4605  rexreusng  4610  reuprg0  4631  rmosn  4648  rabsnifsb  4651  euotd  5395  reuop  6138  wfisg  6177  elfvmptrab1w  6788  elfvmptrab1  6789  ralrnmpt  6856  riotass2  7138  riotass  7139  oprabv  7208  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  ovmpt3rabdm  7398  elovmpt3rab1  7399  tfindes  7571  sbcopeq1a  7742  mpoxopoveq  7879  findcard2  8752  ac6sfi  8756  indexfi  8826  nn0ind-raph  12076  fzrevral  12986  wrdind  14078  wrd2ind  14079  prmind2  16023  elmptrab  22429  isfildlem  22459  2sqreulem4  26024  gropd  26810  grstructd  26811  rspc2daf  30225  opreu2reuALT  30234  ifeqeqx  30291  wrdt2ind  30622  bnj919  32033  bnj976  32044  bnj1468  32113  bnj110  32125  bnj150  32143  bnj151  32144  bnj607  32183  bnj873  32191  bnj849  32192  bnj1388  32300  setinds  33018  dfon2lem1  33023  tfisg  33050  frpoinsg  33076  frinsg  33082  rdgssun  34653  indexdom  35003  sdclem2  35011  sdclem1  35012  fdc1  35015  riotasv2s  36088  elimhyps  36091  sbccomieg  39383  rexrabdioph  39384  rexfrabdioph  39385  aomclem6  39652  pm13.13a  40732  pm13.13b  40733  pm13.14  40734  tratrb  40863  uzwo4  41308  or2expropbilem2  43262  reuf1odnf  43300  ich2exprop  43627  ichnreuop  43628  ichreuopeq  43629  prproropreud  43665  reupr  43678  reuopreuprim  43682