Theorem ndmfv 6866

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 2578	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5847	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6821	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6826	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 182	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃!weu 2569  Vcvv 3430  ∅c0 4274   class class class wbr 5086  dom cdm 5624  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-dm 5634  df-iota 6448  df-fv 6500

This theorem is referenced by:  ndmfvrcl  6867  elfvdm  6868  nfvres  6872  fvfundmfvn0  6874  0fv  6875  funfv  6921  fvun1  6925  fvco4i  6935  fvmpti  6940  mptrcl  6951  fvmptss  6954  fvmptex  6956  fvmptnf  6964  fvmptss2  6968  elfvmptrab1  6970  fvopab4ndm  6972  f0cli  7044  funiunfv  7196  funeldmb  7307  ovprc  7398  oprssdm  7541  nssdmovg  7542  ndmovg  7543  1st2val  7963  2nd2val  7964  brovpreldm  8032  soseq  8102  smofvon2  8289  rdgsucmptnf  8361  frsucmptn  8371  brwitnlem  8435  undifixp  8875  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  10491  alephreg  10496  pwcfsdom  10497  cfpwsdom  10498  adderpq  10870  mulerpq  10871  uzssz  12800  ltweuz  13914  wrdsymb0  14502  lsw0  14518  swrd00  14598  swrd0  14612  pfx00  14628  pfx0  14629  sumz  15675  sumss  15677  sumnul  15713  prod1  15900  prodss  15903  divsfval  17502  cidpropd  17667  lubval  18311  glbval  18324  joinval  18332  meetval  18346  gsumpropd2lem  18638  mulgfval  19036  mpfrcl  22073  iscnp2  23214  setsmstopn  24453  tngtopn  24625  dvbsss  25879  perfdvf  25880  dchrrcl  27217  nofv  27635  ltsres  27640  noseponlem  27642  noextenddif  27646  noextendlt  27647  noextendgt  27648  nolesgn2ores  27650  nogesgn1ores  27652  fvnobday  27656  nosepdmlem  27661  nosepssdm  27664  nosupbnd1lem3  27688  nosupbnd1lem5  27690  nosupbnd2lem1  27693  noinfbnd1lem3  27703  noinfbnd1lem5  27705  noinfbnd2lem1  27708  newval  27841  leftval  27855  rightval  27856  lltr  27868  madess  27872  oldssmade  27873  oldss  27876  lrold  27903  structiedg0val  29105  snstriedgval  29121  rgrx0nd  29678  vsfval  30719  dmadjrnb  31992  hmdmadj  32026  r1wf  35255  rdgprc0  35989  fullfunfv  36145  linedegen  36341  bj-inftyexpitaudisj  37535  bj-inftyexpidisj  37540  bj-fvimacnv0  37616  dibvalrel  41623  dicvalrelN  41645  dihvalrel  41739  itgocn  43610  fpwfvss  43857  r1rankcld  44676  grur1cld  44677  uz0  45858  climfveq  46115  climfveqf  46126  afv2ndeffv0  47720  fvmptrabdm  47753  fvconstr  49349  fvconstrn0  49350  fvconstr2  49351  fvconst0ci  49378  fvconstdomi  49379  ipolub00  49480  oppfrcl  49615  initopropdlemlem  49726  initopropd  49730  termopropd  49731  zeroopropd  49732  fucofvalne  49812