Theorem reldmmpt2 6413

Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014.)

Hypothesis

Ref	Expression
rngop.1

Assertion

Ref	Expression
reldmmpt2

Distinct variable groups:   ,   ,

Proof of Theorem reldmmpt2

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldmoprab 6387	. 2
2		rngop.1	. . . . 5
3		df-mpt2 6301	. . . . 5
4	2, 3	eqtri 2486	. . . 4
5	4	dmeqi 5209	. . 3
6	5	releqi 5091	. 2
7	1, 6	mpbir 209	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  domcdm 5004  Relwrel 5009  {coprab 6297  e.cmpt2 6298

This theorem is referenced by:  reldmmap  7448  reldmsets  14654  reldmress  14683  reldmprds  14846  gsum0  15905  reldmghm  16266  oppglsm  16662  reldmdprd  17028  reldmlmhm  17671  reldmpsr  18010  reldmmpl  18083  reldmopsr  18138  reldmevls  18186  vr1val  18231  reldmevls1  18354  evl1fval  18364  zrhval  18545  reldmdsmm  18764  frlmrcl  18790  matbas0pc  18911  mdetfval  19088  madufval  19139  qtopres  20199  fgabs  20380  reldmtng  21152  reldmnghm  21219  reldmnmhm  21220  dvbsss  22306  reldmmdeg  22455  reldmresv  27816  mzpmfp  30679  mzpmfpOLD  30680

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-dm 5014  df-oprab 6300  df-mpt2 6301