MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfis3 Structured version   Visualization version   GIF version

Theorem tfis3 7790
Description: Transfinite Induction Schema, using implicit substitution. (Contributed by NM, 4-Nov-2003.)
Hypotheses
Ref Expression
tfis3.1 (𝑥 = 𝑦 → (𝜑𝜓))
tfis3.2 (𝑥 = 𝐴 → (𝜑𝜒))
tfis3.3 (𝑥 ∈ On → (∀𝑦𝑥 𝜓𝜑))
Assertion
Ref Expression
tfis3 (𝐴 ∈ On → 𝜒)
Distinct variable groups:   𝜓,𝑥   𝜑,𝑦   𝜒,𝑥   𝑥,𝐴   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝐴(𝑦)

Proof of Theorem tfis3
StepHypRef Expression
1 tfis3.2 . 2 (𝑥 = 𝐴 → (𝜑𝜒))
2 tfis3.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
3 tfis3.3 . . 3 (𝑥 ∈ On → (∀𝑦𝑥 𝜓𝜑))
42, 3tfis2 7789 . 2 (𝑥 ∈ On → 𝜑)
51, 4vtoclga 3532 1 (𝐴 ∈ On → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  wral 3062  Oncon0 6315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-tr 5221  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-ord 6318  df-on 6319
This theorem is referenced by:  tfisi  7791  tfinds  7792  tfrlem1  8318  naddid1  8625  naddssim  8626  ordtypelem7  9456  rankonidlem  9760  tcrank  9816  infxpenlem  9945  alephle  10020  dfac12lem3  10077  ttukeylem5  10445  ttukeylem6  10446  tskord  10712  grudomon  10749  madebdayim  27201  madebday  27213  aomclem6  41324
  Copyright terms: Public domain W3C validator