Theorem ndmfv 6128

Description: The value of a class outside its domain is the empty set. (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 2482	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5241	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 235	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 147	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6094	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 34	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6097	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 175	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  Vcvv 3173  ∅c0 3874   class class class wbr 4583  dom cdm 5038  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717  ax-pow 4769

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-dm 5048  df-iota 5768  df-fv 5812

This theorem is referenced by:  ndmfvrcl  6129  elfvdm  6130  nfvres  6134  fvfundmfvn0  6136  0fv  6137  funfv  6175  fvun1  6179  fvco4i  6186  fvmpti  6190  mptrcl  6198  fvmptss  6201  fvmptex  6203  fvmptnf  6210  fvmptss2  6212  elfvmptrab1  6213  fvopab4ndm  6215  f0cli  6278  funiunfv  6410  ovprc  6581  oprssdm  6713  nssdmovg  6714  ndmovg  6715  1st2val  7085  2nd2val  7086  brovpreldm  7141  curry1val  7157  curry2val  7161  smofvon2  7340  rdgsucmptnf  7412  frsucmptn  7421  brwitnlem  7474  undifixp  7830  r1tr  8522  rankvaln  8545  cardidm  8668  carden2a  8675  carden2b  8676  carddomi2  8679  sdomsdomcardi  8680  pm54.43lem  8708  alephcard  8776  alephnbtwn  8777  alephgeom  8788  cfub  8954  cardcf  8957  cflecard  8958  cfle  8959  cflim2  8968  cfidm  8980  itunisuc  9124  itunitc1  9125  ituniiun  9127  alephadd  9278  alephreg  9283  pwcfsdom  9284  cfpwsdom  9285  adderpq  9657  mulerpq  9658  uzssz  11583  ltweuz  12622  wrdsymb0  13194  lsw0  13205  swrd00  13270  swrd0  13286  sumz  14300  sumss  14302  sumnul  14333  prod1  14513  prodss  14516  divsfval  16030  cidpropd  16193  arwval  16516  coafval  16537  lubval  16807  glbval  16820  joinval  16828  meetval  16842  gsumpropd2lem  17096  mpfrcl  19339  iscnp2  20853  setsmstopn  22093  tngtopn  22264  pcofval  22618  dvbsss  23472  perfdvf  23473  dchrrcl  24765  eleenn  25576  structiedg0val  25699  snstriedgval  25713  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  vsfval  26872  dmadjrnb  28149  hmdmadj  28183  rdgprc0  30943  soseq  30995  nofv  31054  sltres  31061  noseponlem  31065  bdayelon  31079  fvnobday  31081  fullfunfv  31224  linedegen  31420  bj-inftyexpidisj  32274  dibvalrel  35470  dicvalrelN  35492  dihvalrel  35586  itgocn  36753  climfveq  38736  pfx00  40247  pfx0  40248  rgrx0nd  40794  setrec2lem1  42239