Theorem mpt2ndm0 6848

Description: The value of an operation given by a maps-to rule is the empty set if the arguments are not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.)

Hypothesis

Ref	Expression
mpt2ndm0.f	|- F = ( x e. X , y e. Y |-> C )

Assertion

Ref	Expression
mpt2ndm0	|- ( -. ( V e. X /\ W e. Y ) -> ( V F W ) = (/) )

Distinct variable groups:   x, y, X   x, Y, y

Allowed substitution hints:   C( x, y)   F( x, y)   V( x, y)   W( x, y)

Proof of Theorem mpt2ndm0

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpt2ndm0.f	. . . . 5 |- F = ( x e. X , y e. Y |-> C )
2		df-mpt2 6204	. . . . 5 |- ( x e. X , y e. Y |-> C ) = { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
3	1, 2	eqtri 2483	. . . 4 |- F = { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
4	3	dmeqi 5148	. . 3 |- dom F = dom { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) }
5		dmoprabss 6281	. . 3 |- dom { <. <. x , y >. , z >. | ( ( x e. X /\ y e. Y ) /\ z = C ) } C_ ( X X. Y )
6	4, 5	eqsstri 3493	. 2 |- dom F C_ ( X X. Y )
7		nssdmovg 6354	. 2 |- ( ( dom F C_ ( X X. Y ) /\ -. ( V e. X /\ W e. Y ) ) -> ( V F W ) = (/) )
8	6, 7	mpan 670	1 |- ( -. ( V e. X /\ W e. Y ) -> ( V F W ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   = wceq 1370   e. wcel 1758   C_ wss 3435   (/)c0 3744   X. cxp 4945   dom cdm 4947  (class class class)co 6199   {coprab 6200   |-> cmpt2 6201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-xp 4953  df-dm 4957  df-iota 5488  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204

This theorem is referenced by:  brovex  6849  fullfunc  14934  fthfunc  14935  natfval  14974  evlval  17733  matbas0  18411  matrcl  18436  marrepfval  18497  marepvfval  18502  minmar1fval  18583  hmeofval  19462  nghmfval  20432  uvtxisvtx  23549  uvtx0  23550  uvtx01vtx  23551  elovmpt3imp  30307  2wlkonot3v  30541  2spthonot3v  30542