Theorem sseq2i 3944

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

Syntax hints:   ↔ wb 207   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  sseqtrdi  3955  sseqtri  3963  abss  3993  ssrab  4002  ssindif0  4392  difcom  4416  ssunsn2  4758  ssunpr  4765  sspr  4766  sstp  4767  ssintrab  4901  iunpwss  5036  propssopi  5449  f1imadifssran  6571  ssimaex  6912  elpwun  7712  ssfi  9097  frfi  9185  alephislim  9996  cardaleph  10002  fin1a2lem12  10324  zornn0g  10418  ssxr  11206  nnwo  12854  isstruct  17113  issubmgm  18661  issubm  18762  grpissubg  19113  issubrng  20519  cntzsubrng  20539  islinds  21784  basdif0  22936  tgdif0  22975  cmpsublem  23382  cmpsub  23383  hauscmplem  23389  2ndcctbss  23438  fbncp  23822  cnextfval  24045  eltsms  24116  reconn  24812  cmssmscld  25335  nobdaymin  27763  nocvxminlem  27764  axcontlem3  29053  axcontlem4  29054  umgredg  29225  nbuhgr  29430  uhgrvd00  29621  vtxdginducedm1  29630  chsscon1i  31551  hatomistici  32451  chirredlem4  32482  atabs2i  32491  mdsymlem1  32492  mdsymlem3  32494  mdsymlem6  32497  mdsymlem8  32499  dmdbr5ati  32511  iundifdif  32651  poimir  38020  ismblfin  38028  cossssid2  38925  ntrk0kbimka  44483  ntrclsk3  44514  ntrneicls11  44534  wfaxrep  45438  wfaxsep  45439  abssf  45559  ssrabf  45561  stoweidlem57  46500  ovnsubadd  47015  ovnovollem3  47101  grlimedgclnbgr  48486  linccl  48905  lincdifsn  48915