Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tz6.26 Unicode version

Theorem tz6.26 25388
 Description: All nonempty (possibly proper) subclasses of , which has a well-founded relation , have -minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
tz6.26 Se
Distinct variable groups:   ,   ,   ,

Proof of Theorem tz6.26
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wereu2 4534 . . 3 Se
2 reurex 2879 . . 3
31, 2syl 16 . 2 Se
4 rabeq0 3606 . . . 4
5 dfrab3 3574 . . . . . 6
6 vex 2916 . . . . . . 7
76dfpred2 25358 . . . . . 6
85, 7eqtr4i 2424 . . . . 5
98eqeq1i 2408 . . . 4
104, 9bitr3i 243 . . 3
1110rexbii 2688 . 2
123, 11sylib 189 1 Se
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 359   wceq 1649  cab 2387   wne 2564  wral 2663  wrex 2664  wreu 2665  crab 2667   cin 3276   wss 3277  c0 3585   class class class wbr 4167   Se wse 4494   wwe 4495  cpred 25350 This theorem is referenced by:  tz6.26i  25389  wfi  25390 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-br 4168  df-opab 4222  df-po 4458  df-so 4459  df-fr 4496  df-se 4497  df-we 4498  df-xp 4838  df-cnv 4840  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-pred 25351
 Copyright terms: Public domain W3C validator