Theorem sseq2i 3960

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 3957	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  sseqtrdi  3971  sseqtri  3979  abss  4010  ssrab  4019  ssindif0  4417  difcom  4444  ssunsn2  4788  ssunpr  4794  sspr  4795  sstp  4796  ssintrab  4931  iunpwss  5067  propssopi  5485  ssimaex  6963  elpwun  7768  ssfi  9167  frfi  9255  alephislim  10086  cardaleph  10092  fin1a2lem12  10413  zornn0g  10507  ssxr  11303  nnwo  12962  isstruct  17244  issubmgm  18804  issubm  18911  grpissubg  19270  issubrng  20709  cntzsubrng  20729  rspvalint  21432  islinds  22022  basdif0  23178  tgdif0  23217  cmpsublem  23624  cmpsub  23625  hauscmplem  23631  2ndcctbss  23681  fbncp  24065  cnextfval  24288  eltsms  24359  reconn  25055  cmssmscld  25578  nobdaymin  28018  nocvxminlem  28019  axcontlem3  29423  axcontlem4  29424  umgredg  29595  nbuhgr  29803  uhgrvd00  29994  vtxdginducedm1  30003  chsscon1i  31943  hatomistici  32843  chirredlem4  32874  atabs2i  32883  mdsymlem1  32884  mdsymlem3  32886  mdsymlem6  32889  mdsymlem8  32891  dmdbr5ati  32903  iundifdif  33036  poimir  38402  ismblfin  38410  cossssid2  39306  ntrk0kbimka  44879  ntrclsk3  44910  ntrneicls11  44930  wfaxrep  45817  wfaxsep  45818  abssf  45944  ssrabf  45946  stoweidlem57  46885  ovnsubadd  47400  ovnovollem3  47486  grlimedgclnbgr  48911  linccl  49344  lincdifsn  49354