Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbceqbid Unicode version

Theorem sbceqbid 3334
 Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)
Hypotheses
Ref Expression
sbceqbid.1
sbceqbid.2
Assertion
Ref Expression
sbceqbid
Distinct variable group:   ,

Proof of Theorem sbceqbid
StepHypRef Expression
1 sbceqbid.1 . . 3
2 sbceqbid.2 . . . 4
32abbidv 2593 . . 3
41, 3eleq12d 2539 . 2
5 df-sbc 3328 . 2
6 df-sbc 3328 . 2
74, 5, 63bitr4g 288 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {cab 2442  [.wsbc 3327 This theorem is referenced by:  fpwwe2cbv  9029  fpwwe2lem2  9031  fpwwe2lem3  9032  isprs  15559  isdrs  15563  istos  15665  isdlat  15823  issrg  17159  islmod  17516  fdc  30238  sbccomieg  30726  rexrabdioph  30727  hdmap1ffval  37523  hdmap1fval  37524  hdmapffval  37556  hdmapfval  37557  hgmapffval  37615  hgmapfval  37616 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-sbc 3328
 Copyright terms: Public domain W3C validator