Theorem sseq2i 3593

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

Syntax hints:   ↔ wb 195   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseqtri  3600  syl6sseq  3614  abss  3634  ssrab  3643  ssindif0  3983  difcom  4005  ssunsn2  4299  ssunpr  4305  sspr  4306  sstp  4307  ssintrab  4435  iunpwss  4551  propssopi  4896  dffun2  5814  ssimaex  6173  elpwun  6869  frfi  8090  alephislim  8789  cardaleph  8795  fin1a2lem12  9116  zornn0g  9210  ssxr  9986  nnwo  11629  isstruct  15705  issubm  17170  grpissubg  17437  islinds  19967  basdif0  20568  tgdif0  20607  cmpsublem  21012  cmpsub  21013  hauscmplem  21019  2ndcctbss  21068  fbncp  21453  cnextfval  21676  eltsms  21746  reconn  22439  axcontlem3  25646  axcontlem4  25647  umgredg  25812  chsscon1i  27705  hatomistici  28605  chirredlem4  28636  atabs2i  28645  mdsymlem1  28646  mdsymlem3  28648  mdsymlem6  28651  mdsymlem8  28653  dmdbr5ati  28665  iundifdif  28763  nocvxminlem  31089  nocvxmin  31090  poimir  32612  ismblfin  32620  ntrk0kbimka  37357  ntrclsk3  37388  ntrneicls11  37408  abssf  38326  ssrabf  38329  stoweidlem57  38950  ovnsubadd  39462  ovnovollem3  39548  nbuhgr  40565  uhgrvd00  40750  issubmgm  41579  linccl  41997  lincdifsn  42007