Theorem sbceq1a 3740

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068  [wsbc 3729

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbceq2a  3741  elrabsf  3775  cbvralcsf  3880  reusngf  4619  rexreusng  4624  reuprg0  4647  rmosn  4664  rabsnifsb  4667  euotd  5461  reuop  6251  frpoinsg  6301  elfvmptrab1w  6969  elfvmptrab1  6970  ralrnmpt  7042  riotass2  7347  riotass  7348  oprabv  7420  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  ovmpt3rabdm  7619  elovmpt3rab1  7620  tfisg  7798  tfindes  7807  sbcopeq1a  7995  sbcoteq1a  7997  mpoxopoveq  8162  findcard2  9092  ac6sfi  9187  indexfi  9263  setinds  9661  frinsg  9666  nn0ind-raph  12620  fzrevral  13557  wrdind  14675  wrd2ind  14676  prmind2  16645  elmptrab  23802  isfildlem  23832  2sqreulem4  27431  gropd  29114  grstructd  29115  rspc2daf  32550  opreu2reuALT  32561  ifeqeqx  32627  wrdt2ind  33028  bnj919  34926  bnj976  34936  bnj1468  35004  bnj110  35016  bnj150  35034  bnj151  35035  bnj607  35074  bnj873  35082  bnj849  35083  bnj1388  35191  dfon2lem1  35979  rdgssun  37708  indexdom  38069  sdclem2  38077  sdclem1  38078  fdc1  38081  riotasv2s  39418  elimhyps  39421  sbccomieg  43239  rexrabdioph  43240  rexfrabdioph  43241  aomclem6  43505  pm13.13a  44852  pm13.13b  44853  pm13.14  44854  tratrb  44981  uzwo4  45502  or2expropbilem2  47493  reuf1odnf  47567  ich2exprop  47943  ichnreuop  47944  ichreuopeq  47945  prproropreud  47981  reupr  47994  reuopreuprim  47998