Theorem ndmfv 6872

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 2577	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5853	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	imbitrrid 246	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 152	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6827	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6832	. . 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 2568  Vcvv 3429  ∅c0 4273   class class class wbr 5085  dom cdm 5631  ‘cfv 6498

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 2708  ax-nul 5241  ax-pr 5375

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-dm 5641  df-iota 6454  df-fv 6506

This theorem is referenced by:  ndmfvrcl  6873  elfvdm  6874  nfvres  6878  fvfundmfvn0  6880  0fv  6881  funfv  6927  fvun1  6931  fvco4i  6941  fvmpti  6946  mptrcl  6957  fvmptss  6960  fvmptex  6962  fvmptnf  6970  fvmptss2  6974  elfvmptrab1  6976  fvopab4ndm  6978  f0cli  7050  funiunfv  7203  funeldmb  7314  ovprc  7405  oprssdm  7548  nssdmovg  7549  ndmovg  7550  1st2val  7970  2nd2val  7971  brovpreldm  8039  soseq  8109  smofvon2  8296  rdgsucmptnf  8368  frsucmptn  8378  brwitnlem  8442  undifixp  8882  r1tr  9700  rankvaln  9723  cardidm  9883  carden2a  9890  carden2b  9891  carddomi2  9894  sdomsdomcardi  9895  pm54.43lem  9924  alephcard  9992  alephnbtwn  9993  alephgeom  10004  cfub  10171  cardcf  10174  cflecard  10175  cfle  10176  cflim2  10185  cfidm  10197  itunisuc  10341  itunitc1  10342  ituniiun  10344  alephadd  10500  alephreg  10505  pwcfsdom  10506  cfpwsdom  10507  adderpq  10879  mulerpq  10880  uzssz  12809  ltweuz  13923  wrdsymb0  14511  lsw0  14527  swrd00  14607  swrd0  14621  pfx00  14637  pfx0  14638  sumz  15684  sumss  15686  sumnul  15722  prod1  15909  prodss  15912  divsfval  17511  cidpropd  17676  lubval  18320  glbval  18333  joinval  18341  meetval  18355  gsumpropd2lem  18647  mulgfval  19045  mpfrcl  22063  iscnp2  23204  setsmstopn  24443  tngtopn  24615  dvbsss  25869  perfdvf  25870  dchrrcl  27203  nofv  27621  ltsres  27626  noseponlem  27628  noextenddif  27632  noextendlt  27633  noextendgt  27634  nolesgn2ores  27636  nogesgn1ores  27638  fvnobday  27642  nosepdmlem  27647  nosepssdm  27650  nosupbnd1lem3  27674  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem5  27691  noinfbnd2lem1  27694  newval  27827  leftval  27841  rightval  27842  lltr  27854  madess  27858  oldssmade  27859  oldss  27862  lrold  27889  structiedg0val  29091  snstriedgval  29107  rgrx0nd  29663  vsfval  30704  dmadjrnb  31977  hmdmadj  32011  r1wf  35239  rdgprc0  35973  fullfunfv  36129  linedegen  36325  bj-inftyexpitaudisj  37519  bj-inftyexpidisj  37524  bj-fvimacnv0  37600  dibvalrel  41609  dicvalrelN  41631  dihvalrel  41725  itgocn  43592  fpwfvss  43839  r1rankcld  44658  grur1cld  44659  uz0  45840  climfveq  46097  climfveqf  46108  afv2ndeffv0  47708  fvmptrabdm  47741  fvconstr  49337  fvconstrn0  49338  fvconstr2  49339  fvconst0ci  49366  fvconstdomi  49367  ipolub00  49468  oppfrcl  49603  initopropdlemlem  49714  initopropd  49718  termopropd  49719  zeroopropd  49720  fucofvalne  49800