Theorem ndmfv 3736

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 1531	. . . . . 6 |- (x = A -> (x e. dom F <-> A e. dom F))
2		breq1 2617	. . . . . . 7 |- (x = A -> (xFy <-> AFy))
3	2	exbidv 1277	. . . . . 6 |- (x = A -> (E.y xFy <-> E.y AFy))
4		visset 1809	. . . . . . 7 |- x e. V
5	4	eldm 3302	. . . . . 6 |- (x e. dom F <-> E.y xFy)
6	1, 3, 5	vtoclbg 1844	. . . . 5 |- (A e. V -> (A e. dom F <-> E.y AFy))
7		euex 1392	. . . . 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 3730	. . 3 |- (-. E!y AFy -> (F` A) = (/))
11	9, 10	syl6 22	. 2 |- (A e. V -> (-. A e. dom F -> (F` A) = (/)))
12		fvprc 3712	. . 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   = wceq 954   e. wcel 956  E.wex 978  E!weu 1378  Vcvv 1807  (/)c0 2276   class class class wbr 2614  dom cdm 3165  ` cfv 3177

This theorem is referenced by:  ndmfvrcl 3737  elfvdm 3738  nfvres 3739  funfv 3761  fvco 3765  fvopab4ndm 3775  funiunfv 3857  rdgsucopabn 3938  oprprc1 3975  oprssdm 4033  ndmoprg 4034  ndmoprgOLD 4035  1st2val 4085  2nd2val 4086  r1tr 4634  alephon 4845  alephcard 4847  alephnbtwn 4848  alephgeom 4862  cfub 4888  cardcf 4891  cflecard 4892  cfle 4893  uzssz 6370  alephadd 7532  issubg 8068  0vfval 8177  vsfval 8206  dmadjrnb 9770  hmdmadjt 9803

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-xp 3179  df-cnv 3181  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fv 3193

Copyright terms: Public domain