Theorem sseq2i 3942

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sseqtrdi  3953  sseqtri  3961  abss  3990  ssrab  3999  ssindif0  4420  difcom  4447  ssunsn2  4788  ssunpr  4794  sspr  4795  sstp  4796  ssintrab  4936  iunpwss  5072  propssopi  5487  imadifssrn  6220  ssimaex  7001  elpwun  7815  ssfi  9226  frfi  9314  alephislim  10201  cardaleph  10207  fin1a2lem12  10528  zornn0g  10622  ssxr  11418  nnwo  13080  isstruct  17374  issubmgm  18941  issubm  19048  grpissubg  19407  issubrng  20850  cntzsubrng  20870  rspvalint  21574  islinds  22170  basdif0  23326  tgdif0  23365  cmpsublem  23772  cmpsub  23773  hauscmplem  23779  2ndcctbss  23829  fbncp  24213  cnextfval  24436  eltsms  24507  reconn  25203  cmssmscld  25726  nobdaymin  28196  nocvxminlem  28197  axcontlem3  29601  axcontlem4  29602  umgredg  29773  nbuhgr  29981  uhgrvd00  30172  vtxdginducedm1  30181  chsscon1i  32121  hatomistici  33021  chirredlem4  33052  atabs2i  33061  mdsymlem1  33062  mdsymlem3  33064  mdsymlem6  33067  mdsymlem8  33069  dmdbr5ati  33081  iundifdif  33255  0elscott  35878  fnlfvk30  36068  fnlfvk3n0  36069  poimir  38839  ismblfin  38847  cossssid2  39756  ntrk0kbimka  45300  ntrclsk3  45331  ntrneicls11  45351  wfaxrep  46248  wfaxsep  46249  abssf  46400  ssrabf  46402  stoweidlem57  47340  ovnsubadd  47855  ovnovollem3  47941  grlimedgclnbgr  49366  linccl  49857  lincdifsn  49867