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

Theorem isacn 8426
 Description: The property of being a choice set of length . (Contributed by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
isacn AC
Distinct variable groups:   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem isacn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pweq 4013 . . . . . . 7
21difeq1d 3621 . . . . . 6
32oveq1d 6300 . . . . 5
43raleqdv 3064 . . . 4
54anbi2d 703 . . 3
6 df-acn 8324 . . 3 AC
75, 6elab2g 3252 . 2 AC
8 elex 3122 . . 3
9 biid 236 . . . 4
109baib 901 . . 3
118, 10syl 16 . 2
127, 11sylan9bb 699 1 AC
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1379  wex 1596   wcel 1767  wral 2814  cvv 3113   cdif 3473  c0 3785  cpw 4010  csn 4027  cfv 5588  (class class class)co 6285   cmap 7421  AC wacn 8320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6288  df-acn 8324 This theorem is referenced by:  acni  8427  numacn  8431  finacn  8432  acndom  8433  acndom2  8436  acncc  8821
 Copyright terms: Public domain W3C validator