Theorem relssdmrn 6271

Description: A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) (Proof shortened by SN, 23-Dec-2024.)

Assertion

Ref	Expression
relssdmrn	⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))

Proof of Theorem relssdmrn

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

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (Rel 𝐴 → Rel 𝐴)
2		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	opeldm 5888	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴)
5	2, 3	opelrn 5924	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴)
6	4, 5	opelxpd 5689	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴))
7	6	a1i 11	. 2 ⊢ (Rel 𝐴 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴)))
8	1, 7	relssdv 5763	1 ⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  ⟨cop 4589   × cxp 5648  dom cdm 5650  ran crn 5651  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  resssxp  6272  cnvssrndm  6273  cossxp  6274  relrelss  6275  relfld  6277  fssxp  6737  oprabss  7528  cnvexg  7936  resfunexgALT  7960  cofunexg  7961  fnexALT  7963  funexw  7964  erssxp  8741  ttrclexg  9724  wunco  10818  trclublem  15148  trclubi  15149  trclub  15151  reltrclfv  15170  imasless  17712  sylow2a  19833  gsum2d  20186  znleval  21860  tsmsxp  24474  relfi  33196  fcnvgreu  33266  elrgspnsubrunlem2  33809  relssinxpdmrn  39282  trclubNEW  44619  trrelsuperreldg  44668  trrelsuperrel2dg  44671  relwf  45957  hfrel  46020  ishfstruct  46028