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

Step	Hyp	Ref	Expression
1		sbceqbid.1	. . 3
2		sbceqbid.2	. . . 4
3	2	abbidv 2593	. . 3
4	1, 3	eleq12d 2539	. 2
5		df-sbc 3328	. 2
6		df-sbc 3328	. 2
7	4, 5, 6	3bitr4g 288	1

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