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 3465	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3465	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	opeldm 5898	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑥 ∈ dom 𝐴)
5	2, 3	opelrn 5934	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → 𝑦 ∈ ran 𝐴)
6	4, 5	opelxpd 5701	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴))
7	6	a1i 11	. 2 ⊢ (Rel 𝐴 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ (dom 𝐴 × ran 𝐴)))
8	1, 7	relssdv 5775	1 ⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴))

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3911  ⟨cop 4598   × cxp 5660  dom cdm 5662  ran crn 5663  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5259  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-br 5112  df-opab 5176  df-xp 5668  df-rel 5669  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  resssxp  6272  cnvssrndm  6273  cossxp  6274  relrelss  6275  relfld  6277  fssxp  6734  oprabss  7519  cnvexg  7921  resfunexgALT  7945  cofunexg  7946  fnexALT  7948  funexw  7949  erssxp  8718  ttrclexg  9692  wunco  10718  trclublem  15032  trclubi  15033  trclub  15035  reltrclfv  15054  imasless  17594  sylow2a  19689  gsum2d  20042  znleval  21673  tsmsxp  24281  relfi  32888  fcnvgreu  32958  elrgspnsubrunlem2  33509  relssinxpdmrn  38923  trclubNEW  44272  trrelsuperreldg  44321  trrelsuperrel2dg  44324  relwf  45603