Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnsingle Structured version   Visualization version   Unicode version

Theorem fnsingle 30686
 Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
fnsingle Singleton

Proof of Theorem fnsingle
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difss 3560 . . . . 5
2 df-rel 4841 . . . . 5
31, 2mpbir 213 . . . 4
4 df-singleton 30628 . . . . 5 Singleton
54releqi 4918 . . . 4 Singleton
63, 5mpbir 213 . . 3 Singleton
7 vex 3048 . . . . . . 7
8 vex 3048 . . . . . . 7
97, 8brsingle 30684 . . . . . 6 Singleton
10 vex 3048 . . . . . . 7
117, 10brsingle 30684 . . . . . 6 Singleton
12 eqtr3 2472 . . . . . 6
139, 11, 12syl2anb 482 . . . . 5 Singleton Singleton
1413ax-gen 1669 . . . 4 Singleton Singleton
1514gen2 1670 . . 3 Singleton Singleton
16 dffun2 5592 . . 3 Singleton Singleton Singleton Singleton
176, 15, 16mpbir2an 931 . 2 Singleton
18 eqv 3748 . . 3 Singleton Singleton
19 eqid 2451 . . . . . 6
20 snex 4641 . . . . . . 7
217, 20brsingle 30684 . . . . . 6 Singleton
2219, 21mpbir 213 . . . . 5 Singleton
23 breq2 4406 . . . . . 6 Singleton Singleton
2420, 23spcev 3141 . . . . 5 Singleton Singleton
2522, 24ax-mp 5 . . . 4 Singleton
267eldm 5032 . . . 4 Singleton Singleton
2725, 26mpbir 213 . . 3 Singleton
2818, 27mpgbir 1673 . 2 Singleton
29 df-fn 5585 . 2 Singleton Singleton Singleton
3017, 28, 29mpbir2an 931 1 Singleton
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371  wal 1442   wceq 1444  wex 1663   wcel 1887  cvv 3045   cdif 3401   wss 3404   csymdif 3662  csn 3968   class class class wbr 4402   cep 4743   cid 4744   cxp 4832   cdm 4834   crn 4835   wrel 4839   wfun 5576   wfn 5577   ctxp 30596  Singletoncsingle 30604 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-symdif 3663  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-eprel 4745  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fo 5588  df-fv 5590  df-1st 6793  df-2nd 6794  df-txp 30620  df-singleton 30628 This theorem is referenced by:  fvsingle  30687
 Copyright terms: Public domain W3C validator