Theorem sseq12d 3999

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
sseq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
sseq12d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	sseq1d 3997	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3998	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 281	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  3sstr3d  4012  3sstr4d  4013  ssdifeq0  4431  relcnvtrg  6113  knatar  7104  suppfnss  7849  funsssuppss  7850  smogt  7998  oawordri  8170  omwordi  8191  omwordri  8192  oewordi  8211  oewordri  8212  oeworde  8213  nnawordi  8241  nnmwordi  8255  nnmwordri  8256  sbthlem2  8622  sbth  8631  marypha2lem3  8895  hartogslem1  9000  inf3lem1  9085  tcrank  9307  alephle  9508  cfsmolem  9686  isfin3ds  9745  fin23lem17  9754  fin23lem39  9766  isf32lem1  9769  isf32lem2  9770  isf32lem11  9779  isf33lem  9782  isf34lem7  9795  isf34lem6  9796  fin1a2lem13  9828  itunitc1  9836  dominf  9861  dcomex  9863  axdc2lem  9864  dominfac  9989  fpwwe2cbv  10046  fpwwe2lem2  10048  fpwwecbv  10060  fpwwelem  10061  canthwelem  10066  canthwe  10067  wunex2  10154  swrdval  13999  trcleq2lem  14345  dfrtrcl2  14415  vdwpc  16310  vdwlem1  16311  vdwlem6  16316  vdwlem7  16317  vdwlem8  16318  isstruct2  16487  ressval  16545  mreexexlemd  16909  isacs1i  16922  isssc  17084  ssc2  17086  fullfunc  17170  fthfunc  17171  isps  17806  istsr  17821  isdir  17836  gsumvalx  17880  efgi2  18845  dmdprd  19114  dprdss  19145  dmdprdpr  19165  mhpfval  20326  scmatdmat  21118  basis1  21552  baspartn  21556  eltg  21559  cncls  21876  ispnrm  21941  1stcfb  22047  2ndcctbss  22057  1stcelcls  22063  subislly  22083  kgenidm  22149  ptpjpre1  22173  txcmplem2  22244  flimval  22565  flimcf  22584  fclscf  22627  metss  23112  isngp  23199  iscph  23768  cphsscph  23848  equivcau  23897  caubl  23905  caublcls  23906  ovoliunlem3  24099  volsuplem  24150  volsup  24151  dyaddisj  24191  itg1climres  24309  isausgr  26943  issubgr  27047  subgrprop3  27052  cusgrfilem1  27231  wkslem1  27383  wkslem2  27384  iswlk  27386  wlkres  27446  redwlk  27448  wlkp1lem8  27456  wlkdlem2  27459  crctcshwlkn0lem4  27585  crctcshwlkn0lem5  27586  crctcshwlkn0lem6  27587  2wlkdlem10  27708  3wlkdlem10  27942  eupthseg  27979  issh  28979  isch  28993  hsupss  29112  shslej  29151  shlub  29185  ledi  29311  pjoi0  29488  mdbr4  30069  dmdbr4  30077  dmdi4  30078  dmdbr5  30079  mdslle1i  30088  mdslle2i  30089  mdslmd1lem1  30096  mdslmd1lem2  30097  mdslmd1lem3  30098  mdslmd1lem4  30099  mdslmd1i  30100  sumdmdlem2  30190  resvval  30895  zhmnrg  31203  ispisys  31406  pfxwlk  32365  cvmliftlem3  32529  ismfs  32791  rdgssun  34653  poimirlem32  34918  volsupnfl  34931  elrefrels2  35751  refreleq  35754  elcnvrefrels2  35764  dfsymrels2  35775  dfsymrel2  35779  elsymrels2  35783  symreleq  35788  elrefsymrels2  35799  dftrrels2  35805  dftrrel2  35807  eltrrels2  35809  trreleq  35812  eleqvrels2  35821  lssatle  36145  pmaple  36891  2polcon4bN  37048  ispautN  37229  diaord  38177  dibord  38289  dihord6apre  38386  dihord3  38387  dihord4  38388  dihcnvord  38404  dvh4dimlem  38573  islpolN  38613  mapdordlem2  38767  mapdcnvordN  38788  mapdindp  38801  hdmaplkr  39043  ismrcd1  39288  ismrcd2  39289  ismrc  39291  incssnn0  39301  diophrw  39349  hbtlem5  39721  hbt  39723  rclexi  39968  rtrclex  39970  trclubgNEW  39971  rtrclexi  39974  cnvrcl0  39978  cnvtrcl0  39979  dfrtrcl5  39982  trcleq2lemRP  39983  trficl  40007  dfrcl2  40012  relexpss1d  40043  trclrelexplem  40049  brtrclfv2  40065  dfrtrcl3  40071  heeq12  40115  sscon34b  40362  ntrk2imkb  40380  clsk3nimkb  40383  clsk1independent  40389  isotone1  40391  isotone2  40392  ntrclsss  40406  ntrclsiso  40410  ntrclsk2  40411  ntrclsk3  40413  scottabf  40569  ismnu  40590  nzss  40642  iunincfi  41353  fourierdlem89  42474  fourierdlem90  42475  fourierdlem91  42476  meaiuninclem  42756  meaiunincf  42759  meaiuninc3v  42760  meaiuninc3  42761  meaiininclem  42762  meaiininc  42763  caragenss  42780  carageniuncllem1  42797  ovnsslelem  42836  hoidmvle  42876  ovnhoilem2  42878  hoiqssbl  42901  ovolval5lem2  42929  ovolval5lem3  42930  vonioolem2  42957  vonicclem2  42960  uspgrsprf  44015  scmsuppss  44414