Theorem ndmfv 6859

Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995.)

Assertion

Ref	Expression
ndmfv	⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Proof of Theorem ndmfv

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		euex 2570	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5845	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6814	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6818	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 182	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃!weu 2561  Vcvv 3438  ∅c0 4286   class class class wbr 5095  dom cdm 5623  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-dm 5633  df-iota 6442  df-fv 6494

This theorem is referenced by:  ndmfvrcl  6860  elfvdm  6861  nfvres  6865  fvfundmfvn0  6867  0fv  6868  funfv  6914  fvun1  6918  fvco4i  6928  fvmpti  6933  mptrcl  6943  fvmptss  6946  fvmptex  6948  fvmptnf  6956  fvmptss2  6960  elfvmptrab1  6962  fvopab4ndm  6964  f0cli  7036  funiunfv  7188  funeldmb  7300  ovprc  7391  oprssdm  7534  nssdmovg  7535  ndmovg  7536  1st2val  7959  2nd2val  7960  brovpreldm  8029  soseq  8099  smofvon2  8286  rdgsucmptnf  8358  frsucmptn  8368  brwitnlem  8432  undifixp  8868  r1tr  9691  rankvaln  9714  cardidm  9874  carden2a  9881  carden2b  9882  carddomi2  9885  sdomsdomcardi  9886  pm54.43lem  9915  alephcard  9983  alephnbtwn  9984  alephgeom  9995  cfub  10162  cardcf  10165  cflecard  10166  cfle  10167  cflim2  10176  cfidm  10188  itunisuc  10332  itunitc1  10333  ituniiun  10335  alephadd  10490  alephreg  10495  pwcfsdom  10496  cfpwsdom  10497  adderpq  10869  mulerpq  10870  uzssz  12775  ltweuz  13887  wrdsymb0  14475  lsw0  14491  swrd00  14570  swrd0  14584  pfx00  14600  pfx0  14601  sumz  15648  sumss  15650  sumnul  15686  prod1  15870  prodss  15873  divsfval  17470  cidpropd  17635  lubval  18279  glbval  18292  joinval  18300  meetval  18314  gsumpropd2lem  18572  mulgfval  18967  mpfrcl  22009  iscnp2  23143  setsmstopn  24383  tngtopn  24555  dvbsss  25820  perfdvf  25821  dchrrcl  27168  nofv  27586  sltres  27591  noseponlem  27593  noextenddif  27597  noextendlt  27598  noextendgt  27599  nolesgn2ores  27601  nogesgn1ores  27603  fvnobday  27607  nosepdmlem  27612  nosepssdm  27615  nosupbnd1lem3  27639  nosupbnd1lem5  27641  nosupbnd2lem1  27644  noinfbnd1lem3  27654  noinfbnd1lem5  27656  noinfbnd2lem1  27659  newval  27784  leftval  27792  rightval  27793  lltropt  27805  madess  27809  oldssmade  27810  oldss  27811  lrold  27830  structiedg0val  28986  snstriedgval  29002  rgrx0nd  29559  vsfval  30596  dmadjrnb  31869  hmdmadj  31903  rdgprc0  35786  fullfunfv  35940  linedegen  36136  bj-inftyexpitaudisj  37198  bj-inftyexpidisj  37203  bj-fvimacnv0  37279  dibvalrel  41162  dicvalrelN  41184  dihvalrel  41278  itgocn  43157  fpwfvss  43405  r1rankcld  44224  grur1cld  44225  uz0  45411  climfveq  45670  climfveqf  45681  afv2ndeffv0  47264  fvmptrabdm  47297  fvconstr  48866  fvconstrn0  48867  fvconstr2  48868  fvconst0ci  48895  fvconstdomi  48896  ipolub00  48997  oppfrcl  49133  initopropdlemlem  49244  initopropd  49248  termopropd  49249  zeroopropd  49250  fucofvalne  49330