Theorem sseq2i 3951

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

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

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 2708

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

This theorem is referenced by:  sseqtrdi  3962  sseqtri  3970  abss  4002  ssrab  4011  ssindif0  4404  difcom  4428  ssunsn2  4770  ssunpr  4777  sspr  4778  sstp  4779  ssintrab  4913  iunpwss  5049  propssopi  5462  f1imadifssran  6584  ssimaex  6925  elpwun  7723  ssfi  9107  frfi  9195  alephislim  10005  cardaleph  10011  fin1a2lem12  10333  zornn0g  10427  ssxr  11215  nnwo  12863  isstruct  17122  issubmgm  18670  issubm  18771  grpissubg  19122  issubrng  20524  cntzsubrng  20544  islinds  21789  basdif0  22918  tgdif0  22957  cmpsublem  23364  cmpsub  23365  hauscmplem  23371  2ndcctbss  23420  fbncp  23804  cnextfval  24027  eltsms  24098  reconn  24794  cmssmscld  25317  nobdaymin  27745  nocvxminlem  27746  axcontlem3  29035  axcontlem4  29036  umgredg  29207  nbuhgr  29412  uhgrvd00  29603  vtxdginducedm1  29612  chsscon1i  31533  hatomistici  32433  chirredlem4  32464  atabs2i  32473  mdsymlem1  32474  mdsymlem3  32476  mdsymlem6  32479  mdsymlem8  32481  dmdbr5ati  32493  iundifdif  32632  poimir  37974  ismblfin  37982  cossssid2  38879  ntrk0kbimka  44466  ntrclsk3  44497  ntrneicls11  44517  wfaxrep  45421  wfaxsep  45422  abssf  45542  ssrabf  45544  stoweidlem57  46485  ovnsubadd  47000  ovnovollem3  47086  grlimedgclnbgr  48471  linccl  48890  lincdifsn  48900