Theorem ndmfv 6700

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 2662	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥)
2		eldmg 5767	. . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥))
3	1, 2	syl5ibr 248	. . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹))
4	3	con3d 155	. . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥))
5		tz6.12-2 6660	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
6	4, 5	syl6 35	. 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
7		fvprc 6663	. . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)
8	7	a1d 25	. 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅))
9	6, 8	pm2.61i 184	1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃!weu 2653  Vcvv 3494  ∅c0 4291   class class class wbr 5066  dom cdm 5555  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210  ax-pow 5266

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-dm 5565  df-iota 6314  df-fv 6363

This theorem is referenced by:  ndmfvrcl  6701  elfvdm  6702  nfvres  6706  fvfundmfvn0  6708  0fv  6709  funfv  6750  fvun1  6754  fvco4i  6762  fvmpti  6767  mptrcl  6777  fvmptss  6780  fvmptex  6782  fvmptnf  6790  fvmptss2  6793  elfvmptrab1  6795  fvopab4ndm  6797  f0cli  6864  funiunfv  7007  ovprc  7194  oprssdm  7329  nssdmovg  7330  ndmovg  7331  1st2val  7717  2nd2val  7718  brovpreldm  7784  smofvon2  7993  rdgsucmptnf  8065  frsucmptn  8074  brwitnlem  8132  undifixp  8498  r1tr  9205  rankvaln  9228  cardidm  9388  carden2a  9395  carden2b  9396  carddomi2  9399  sdomsdomcardi  9400  pm54.43lem  9428  alephcard  9496  alephnbtwn  9497  alephgeom  9508  cfub  9671  cardcf  9674  cflecard  9675  cfle  9676  cflim2  9685  cfidm  9697  itunisuc  9841  itunitc1  9842  ituniiun  9844  alephadd  9999  alephreg  10004  pwcfsdom  10005  cfpwsdom  10006  adderpq  10378  mulerpq  10379  uzssz  12265  ltweuz  13330  wrdsymb0  13901  lsw0  13917  swrd00  14006  swrd0  14020  pfx00  14036  pfx0  14037  sumz  15079  sumss  15081  sumnul  15115  prod1  15298  prodss  15301  divsfval  16820  cidpropd  16980  lubval  17594  glbval  17607  joinval  17615  meetval  17629  gsumpropd2lem  17889  mulgfval  18226  mpfrcl  20298  iscnp2  21847  setsmstopn  23088  tngtopn  23259  dvbsss  24500  perfdvf  24501  dchrrcl  25816  structiedg0val  26807  snstriedgval  26823  rgrx0nd  27376  vsfval  28410  dmadjrnb  29683  hmdmadj  29717  funeldmb  33006  rdgprc0  33038  soseq  33096  nofv  33164  sltres  33169  noseponlem  33171  noextenddif  33175  noextendlt  33176  noextendgt  33177  nolesgn2ores  33179  fvnobday  33183  nosepdmlem  33187  nosepssdm  33190  nosupbnd1lem3  33210  nosupbnd1lem5  33212  nosupbnd2lem1  33215  fullfunfv  33408  linedegen  33604  bj-inftyexpitaudisj  34490  bj-inftyexpidisj  34495  bj-fvimacnv0  34571  dibvalrel  38314  dicvalrelN  38336  dihvalrel  38430  itgocn  39813  r1rankcld  40616  grur1cld  40617  uz0  41735  climfveq  41999  climfveqf  42010  afv2ndeffv0  43508  fvmptrabdm  43541  setrec2lem1  44845