Theorem sseq2i 3965

Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sseq2i	⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Proof of Theorem sseq2i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq2 3962	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3903

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-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  sseqtrdi  3976  sseqtri  3984  abss  4016  ssrab  4025  ssindif0  4418  difcom  4443  ssunsn2  4785  ssunpr  4792  sspr  4793  sstp  4794  ssintrab  4928  iunpwss  5064  propssopi  5464  f1imadifssran  6586  ssimaex  6927  elpwun  7724  ssfi  9109  frfi  9197  alephislim  10005  cardaleph  10011  fin1a2lem12  10333  zornn0g  10427  ssxr  11214  nnwo  12838  isstruct  17091  issubmgm  18639  issubm  18740  grpissubg  19088  issubrng  20492  cntzsubrng  20512  islinds  21776  basdif0  22909  tgdif0  22948  cmpsublem  23355  cmpsub  23356  hauscmplem  23362  2ndcctbss  23411  fbncp  23795  cnextfval  24018  eltsms  24089  reconn  24785  cmssmscld  25318  nobdaymin  27761  nocvxminlem  27762  axcontlem3  29051  axcontlem4  29052  umgredg  29223  nbuhgr  29428  uhgrvd00  29620  vtxdginducedm1  29629  chsscon1i  31549  hatomistici  32449  chirredlem4  32480  atabs2i  32489  mdsymlem1  32490  mdsymlem3  32492  mdsymlem6  32495  mdsymlem8  32497  dmdbr5ati  32509  iundifdif  32648  poimir  37901  ismblfin  37909  cossssid2  38806  ntrk0kbimka  44392  ntrclsk3  44423  ntrneicls11  44443  wfaxrep  45347  wfaxsep  45348  abssf  45468  ssrabf  45470  stoweidlem57  46412  ovnsubadd  46927  ovnovollem3  47013  grlimedgclnbgr  48352  linccl  48771  lincdifsn  48781