Theorem ndmfv 3684

Description: The value of a class outside its domain is the empty set.

Assertion

Ref	Expression
ndmfv	|- (-. A e. dom F -> (F` A) = (/))

Proof of Theorem ndmfv

Step	Hyp	Ref	Expression
1		eleq1 1510	. . . . . 6 |- (x = A -> (x e. dom F <-> A e. dom F))
2		breq1 2590	. . . . . . 7 |- (x = A -> (xFy <-> AFy))
3	2	exbidv 1261	. . . . . 6 |- (x = A -> (E.y xFy <-> E.y AFy))
4		visset 1788	. . . . . . 7 |- x e. V
5	4	eldm 3264	. . . . . 6 |- (x e. dom F <-> E.y xFy)
6	1, 3, 5	vtoclbg 1823	. . . . 5 |- (A e. V -> (A e. dom F <-> E.y AFy))
7		euex 1371	. . . . 5 |- (E!y AFy -> E.y AFy)
8	6, 7	syl5bir 210	. . . 4 |- (A e. V -> (E!y AFy -> A e. dom F))
9	8	con3d 95	. . 3 |- (A e. V -> (-. A e. dom F -> -. E!y AFy))
10		tz6.12-2 3678	. . 3 |- (-. E!y AFy -> (F` A) = (/))
11	9, 10	syl6 22	. 2 |- (A e. V -> (-. A e. dom F -> (F` A) = (/)))
12		fvprc 3660	. . 3 |- (-. A e. V -> (F` A) = (/))
13	12	a1d 12	. 2 |- (-. A e. V -> (-. A e. dom F -> (F` A) = (/)))
14	11, 13	pm2.61i 126	1 |- (-. A e. dom F -> (F` A) = (/))

Syntax hints:  -. wn 2   -> wi 3  E.wex 956   = wceq 1099   e. wcel 1105  E!weu 1357  Vcvv 1786  (/)c0 2251   class class class wbr 2587  dom cdm 3133  ` cfv 3145

This theorem is referenced by:  ndmfvrcl 3685  elfvdm 3686  nfvres 3687  funfv 3709  fvco 3713  fvopab4ndm 3723  funiunfv 3805  rdgsucopabn 3886  oprprc1 3923  oprssdm 3981  ndmoprg 3982  ndmoprgOLD 3983  1st2val 4033  2nd2val 4034  r1tr 4578  alephon 4788  alephcard 4790  alephnbtwn 4791  alephgeom 4805  cfub 4831  cardcf 4834  cflecard 4835  cfle 4836  uzssz 6313  alephadd 7475  issubg 8001  0vfval 8105  vsfval 8132  dmadjrnb 9961  hmdmadjt 9994

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384  df-op 2387  df-uni 2472  df-br 2588  df-opab 2635  df-xp 3147  df-cnv 3149  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fv 3161

Copyright terms: Public domain