Theorem sbceq1a 3731

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  [wsb 2069  [wsbc 3720

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sbc 3721

This theorem is referenced by:  sbceq2a  3732  elrabsf  3764  cbvralcsf  3870  vtocl2dOLD  3876  reusngf  4572  rexreusng  4577  reuprg0  4598  rmosn  4615  rabsnifsb  4618  euotd  5368  reuop  6112  wfisg  6151  elfvmptrab1w  6771  elfvmptrab1  6772  ralrnmpt  6839  riotass2  7123  riotass  7124  oprabv  7193  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  ovmpt3rabdm  7384  elovmpt3rab1  7385  tfindes  7557  sbcopeq1a  7730  mpoxopoveq  7868  findcard2  8742  ac6sfi  8746  indexfi  8816  nn0ind-raph  12070  fzrevral  12987  wrdind  14075  wrd2ind  14076  prmind2  16019  elmptrab  22432  isfildlem  22462  2sqreulem4  26038  gropd  26824  grstructd  26825  rspc2daf  30238  opreu2reuALT  30247  ifeqeqx  30309  wrdt2ind  30653  bnj919  32148  bnj976  32159  bnj1468  32228  bnj110  32240  bnj150  32258  bnj151  32259  bnj607  32298  bnj873  32306  bnj849  32307  bnj1388  32415  setinds  33136  dfon2lem1  33141  tfisg  33168  frpoinsg  33194  frinsg  33200  rdgssun  34795  indexdom  35172  sdclem2  35180  sdclem1  35181  fdc1  35184  riotasv2s  36254  elimhyps  36257  sbccomieg  39734  rexrabdioph  39735  rexfrabdioph  39736  aomclem6  40003  pm13.13a  41111  pm13.13b  41112  pm13.14  41113  tratrb  41242  uzwo4  41687  or2expropbilem2  43625  reuf1odnf  43663  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990  prproropreud  44026  reupr  44039  reuopreuprim  44043