MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfrel2 Unicode version

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

Proof of Theorem dfrel2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relcnv 5379 . . 3
2 vex 3112 . . . . . 6
3 vex 3112 . . . . . 6
42, 3opelcnv 5189 . . . . 5
53, 2opelcnv 5189 . . . . 5
64, 5bitri 249 . . . 4
76eqrelriv 5101 . . 3
81, 7mpan 670 . 2
9 releq 5090 . . 3
101, 9mpbii 211 . 2
118, 10impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  <.cop 4035  `'ccnv 5003  Relwrel 5009
This theorem is referenced by:  dfrel4v  5463  cnvcnv  5464  cnveqb  5467  dfrel3  5469  cnvcnvres  5476  cnvsn  5496  cores2  5525  co01  5527  coi2  5529  relcnvtr  5532  funcnvres2  5664  f1cnvcnv  5794  f1ocnv  5833  f1ocnvb  5834  f1ococnv1  5849  isores1  6230  relcnvexb  6748  cnvf1o  6899  fnwelem  6915  tposf12  6999  ssenen  7711  cantnffval2  8135  cantnffval2OLD  8157  fsumcnv  13588  fprodcnv  13787  structcnvcnv  14643  imasless  14937  oppcinv  15170  cnvps  15842  cnvpsb  15843  cnvtsr  15852  gimcnv  16315  lmimcnv  17713  hmeocnv  20263  hmeocnvb  20275  cmphaushmeo  20301  ustexsym  20718  pi1xfrcnv  21557  dvlog  23032  efopnlem2  23038  fimacnvinrn  27475  gtiso  27519  relexprel  29057  f1ocan2fv  30218  ltrncnvnid  35851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-cnv 5012
  Copyright terms: Public domain W3C validator