Theorem dfrel2 6153

Description: Alternate definition of relation. Exercise 2 of [TakeutiZaring] p. 25. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
dfrel2	⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Proof of Theorem dfrel2

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

Step	Hyp	Ref	Expression
1		relcnv 6069	. . 3 ⊢ Rel ◡◡𝑅
2		vex 3433	. . . . . 6 ⊢ 𝑥 ∈ V
3		vex 3433	. . . . . 6 ⊢ 𝑦 ∈ V
4	2, 3	opelcnv 5836	. . . . 5 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ ◡𝑅)
5	3, 2	opelcnv 5836	. . . . 5 ⊢ (⟨𝑦, 𝑥⟩ ∈ ◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
6	4, 5	bitri 275	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ ◡◡𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
7	6	eqrelriv 5745	. . 3 ⊢ ((Rel ◡◡𝑅 ∧ Rel 𝑅) → ◡◡𝑅 = 𝑅)
8	1, 7	mpan 691	. 2 ⊢ (Rel 𝑅 → ◡◡𝑅 = 𝑅)
9		releq 5733	. . 3 ⊢ (◡◡𝑅 = 𝑅 → (Rel ◡◡𝑅 ↔ Rel 𝑅))
10	1, 9	mpbii 233	. 2 ⊢ (◡◡𝑅 = 𝑅 → Rel 𝑅)
11	8, 10	impbii 209	1 ⊢ (Rel 𝑅 ↔ ◡◡𝑅 = 𝑅)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ⟨cop 4573  ^◡ccnv 5630  Rel wrel 5636

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638  df-cnv 5639

This theorem is referenced by:  dfrel4v  6154  cnvcnv  6156  cnveqb  6160  dfrel3  6162  cnvcnvres  6169  cnvsng  6187  cores2  6224  co01  6226  coi2  6228  relcnvtrg  6231  funcnvres2  6578  f1cnvcnv  6745  f1ocnv  6792  f1ocnvb  6793  f1ococnv1  6809  fimacnvinrn  7023  isores1  7289  relcnvexb  7877  cnvf1o  8061  fnwelem  8081  tposf12  8201  ssenen  9089  f1oenfirn  9114  f1domfi  9115  cantnffval2  9616  fsumcnv  15735  fprodcnv  15948  structcnvcnv  17123  imasless  17504  oppcinv  17747  cnvps  18544  cnvpsb  18545  cnvtsr  18554  gimcnv  19242  rngimcnv  20436  lmimcnv  21062  hmeocnv  23727  hmeocnvb  23739  cmphaushmeo  23765  ustexsym  24181  pi1xfrcnv  25024  dvlog  26615  efopnlem2  26621  gtiso  32774  cycpmconjvlem  33202  cycpmconjs  33217  f1ocan2fv  38048  relcnveq3  38648  relcnveq2  38650  brcnvrabga  38663  dfrel5  38667  elrelscnveq3  38948  elrelscnveq2  38950  ltrncnvnid  40573  rimcnv  42962  relintab  44010  cnvssb  44013  relnonrel  44014  cononrel1  44021  cononrel2  44022  clrellem  44049  clcnvlem  44050  relexpaddss  44145  3f1oss1  47523  3f1oss2  47524  tposideq  49363