Theorem dmss 5478

Description: Subset theorem for domain. (Contributed by NM, 11-Aug-1994.)

Assertion

Ref	Expression
dmss	⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Proof of Theorem dmss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3738	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	eximdv 1995	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴 → ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		vex 3343	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5477	. . 3 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐴)
5	3	eldm2 5477	. . 3 ⊢ (𝑥 ∈ dom 𝐵 ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	2, 4, 5	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ dom 𝐴 → 𝑥 ∈ dom 𝐵))
7	6	ssrdv 3750	1 ⊢ (𝐴 ⊆ 𝐵 → dom 𝐴 ⊆ dom 𝐵)

Syntax hints:   → wi 4  ∃wex 1853   ∈ wcel 2139   ⊆ wss 3715  ⟨cop 4327  dom cdm 5266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-dm 5276

This theorem is referenced by:  dmeq  5479  dmv  5496  rnss  5509  dmiin  5524  ssxpb  5726  sofld  5739  relrelss  5820  funssxp  6222  fndmdif  6484  fneqeql2  6489  dff3  6535  frxp  7455  fnwelem  7460  funsssuppss  7490  tposss  7522  wfrlem16  7599  smores  7618  smores2  7620  tfrlem13  7655  imafi  8424  hartogslem1  8612  wemapso  8621  r0weon  9025  infxpenlem  9026  brdom3  9542  brdom5  9543  brdom4  9544  fpwwe2lem13  9656  fpwwe2  9657  canth4  9661  canthwelem  9664  pwfseqlem4  9676  nqerf  9944  dmrecnq  9982  uzrdgfni  12951  hashdmpropge2  13457  dmtrclfv  13958  rlimpm  14430  isstruct2  16069  strlemor1OLD  16171  strleun  16174  imasaddfnlem  16390  imasvscafn  16399  isohom  16637  catcoppccl  16959  tsrss  17424  ledm  17425  dirdm  17435  f1omvdmvd  18063  mvdco  18065  f1omvdconj  18066  pmtrfb  18085  pmtrfconj  18086  symggen  18090  symggen2  18091  pmtrdifellem1  18096  pmtrdifellem2  18097  psgnunilem1  18113  gsum2d  18571  lspextmo  19258  dsmmfi  20284  lindfres  20364  mdetdiaglem  20606  tsmsxp  22159  ustssco  22219  setsmstopn  22484  metustexhalf  22562  tngtopn  22655  equivcau  23298  cmetss  23313  dvbssntr  23863  pserdv  24382  structgrssvtxlemOLD  26114  subgreldmiedg  26374  hlimcaui  28402  metideq  30245  esum2d  30464  fundmpss  31971  fixssdm  32319  filnetlem3  32681  filnetlem4  32682  ssbnd  33900  bnd2lem  33903  ismrcd1  37763  istopclsd  37765  mptrcllem  38422  cnvrcl0  38434  dmtrcl  38436  dfrcl2  38468  relexpss1d  38499  rp-imass  38567  rfovcnvf1od  38800  fourierdlem80  40906  issmflem  41442