Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supp0prc Structured version   Unicode version

Theorem supp0prc 6924
 Description: The support of a class is empty if either the class or the "zero" is a proper class. . (Contributed by AV, 28-May-2019.)
Assertion
Ref Expression
supp0prc supp

Proof of Theorem supp0prc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-supp 6922 . 2 supp
21mpt2ndm0 6520 1 supp
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 370   wceq 1437   wcel 1868   wne 2618  crab 2779  cvv 3081  c0 3761  csn 3996   cdm 4849  cima 4852  (class class class)co 6301   supp csupp 6921 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-xp 4855  df-dm 4859  df-iota 5561  df-fv 5605  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-supp 6922 This theorem is referenced by:  suppssdm  6934  suppun  6942  extmptsuppeq  6946  funsssuppss  6948  fczsupp0  6951  suppss  6952  suppssov1  6954  suppss2  6956  suppssfv  6958  supp0cosupp0  6961  imacosupp  6962  fsuppun  7904
 Copyright terms: Public domain W3C validator