Theorem sseq12d 3948

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 3946	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3947	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 282	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  3sstr3d  3961  3sstr4d  3962  sscon34b  4219  ssdifeq0  4390  relcnvtrg  6086  knatar  7089  suppfnss  7838  funsssuppss  7839  smogt  7987  oawordri  8159  omwordi  8180  omwordri  8181  oewordi  8200  oewordri  8201  oeworde  8202  nnawordi  8230  nnmwordi  8244  nnmwordri  8245  sbthlem2  8612  sbth  8621  marypha2lem3  8885  hartogslem1  8990  inf3lem1  9075  tcrank  9297  alephle  9499  cfsmolem  9681  isfin3ds  9740  fin23lem17  9749  fin23lem39  9761  isf32lem1  9764  isf32lem2  9765  isf32lem11  9774  isf33lem  9777  isf34lem7  9790  isf34lem6  9791  fin1a2lem13  9823  itunitc1  9831  dominf  9856  dcomex  9858  axdc2lem  9859  dominfac  9984  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  wunex2  10149  swrdval  13996  trcleq2lem  14342  dfrtrcl2  14413  vdwpc  16306  vdwlem1  16307  vdwlem6  16312  vdwlem7  16313  vdwlem8  16314  isstruct2  16485  ressval  16543  mreexexlemd  16907  isacs1i  16920  isssc  17082  ssc2  17084  fullfunc  17168  fthfunc  17169  isps  17804  istsr  17819  isdir  17834  gsumvalx  17878  efgi2  18843  dmdprd  19113  dprdss  19144  dmdprdpr  19164  mhpfval  20791  scmatdmat  21120  basis1  21555  baspartn  21559  eltg  21562  cncls  21879  ispnrm  21944  1stcfb  22050  2ndcctbss  22060  1stcelcls  22066  subislly  22086  kgenidm  22152  ptpjpre1  22176  txcmplem2  22247  flimval  22568  flimcf  22587  fclscf  22630  metss  23115  isngp  23202  iscph  23775  cphsscph  23855  equivcau  23904  caubl  23912  caublcls  23913  ovoliunlem3  24108  volsuplem  24159  volsup  24160  dyaddisj  24200  itg1climres  24318  isausgr  26957  issubgr  27061  subgrprop3  27066  cusgrfilem1  27245  wkslem1  27397  wkslem2  27398  iswlk  27400  wlkres  27460  redwlk  27462  wlkp1lem8  27470  wlkdlem2  27473  crctcshwlkn0lem4  27599  crctcshwlkn0lem5  27600  crctcshwlkn0lem6  27601  2wlkdlem10  27721  3wlkdlem10  27954  eupthseg  27991  issh  28991  isch  29005  hsupss  29124  shslej  29163  shlub  29197  ledi  29323  pjoi0  29500  mdbr4  30081  dmdbr4  30089  dmdi4  30090  dmdbr5  30091  mdslle1i  30100  mdslle2i  30101  mdslmd1lem1  30108  mdslmd1lem2  30109  mdslmd1lem3  30110  mdslmd1lem4  30111  mdslmd1i  30112  sumdmdlem2  30202  resvval  30951  zhmnrg  31318  ispisys  31521  pfxwlk  32483  cvmliftlem3  32647  ismfs  32909  rdgssun  34795  poimirlem32  35089  volsupnfl  35102  elrefrels2  35917  refreleq  35920  elcnvrefrels2  35930  dfsymrels2  35941  dfsymrel2  35945  elsymrels2  35949  symreleq  35954  elrefsymrels2  35965  dftrrels2  35971  dftrrel2  35973  eltrrels2  35975  trreleq  35978  eleqvrels2  35987  lssatle  36311  pmaple  37057  2polcon4bN  37214  ispautN  37395  diaord  38343  dibord  38455  dihord6apre  38552  dihord3  38553  dihord4  38554  dihcnvord  38570  dvh4dimlem  38739  islpolN  38779  mapdordlem2  38933  mapdcnvordN  38954  mapdindp  38967  hdmaplkr  39209  ismrcd1  39639  ismrcd2  39640  ismrc  39642  incssnn0  39652  diophrw  39700  hbtlem5  40072  hbt  40074  rclexi  40315  rtrclex  40317  trclubgNEW  40318  rtrclexi  40321  cnvrcl0  40325  cnvtrcl0  40326  dfrtrcl5  40329  trcleq2lemRP  40330  trficl  40370  dfrcl2  40375  relexpss1d  40406  trclrelexplem  40412  brtrclfv2  40428  dfrtrcl3  40434  heeq12  40477  ntrk2imkb  40740  clsk3nimkb  40743  clsk1independent  40749  isotone1  40751  isotone2  40752  ntrclsss  40766  ntrclsiso  40770  ntrclsk2  40771  ntrclsk3  40773  scottabf  40948  ismnu  40969  nzss  41021  iunincfi  41730  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  meaiuninclem  43119  meaiunincf  43122  meaiuninc3v  43123  meaiuninc3  43124  meaiininclem  43125  meaiininc  43126  caragenss  43143  carageniuncllem1  43160  ovnsslelem  43199  hoidmvle  43239  ovnhoilem2  43241  hoiqssbl  43264  ovolval5lem2  43292  ovolval5lem3  43293  vonioolem2  43320  vonicclem2  43323  uspgrsprf  44374  scmsuppss  44774