ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zfregfr GIF version

Theorem zfregfr 4594
Description: The epsilon relation is well-founded on any class. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
zfregfr E Fr 𝐴

Proof of Theorem zfregfr
Dummy variables 𝑠 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-frind 4353 . 2 ( E Fr 𝐴 ↔ ∀𝑠 FrFor E 𝐴𝑠)
2 bi2.04 248 . . . . . . 7 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) ↔ (𝑥𝐴 → (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠)))
32albii 1481 . . . . . 6 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) ↔ ∀𝑥(𝑥𝐴 → (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠)))
4 df-ral 2473 . . . . . 6 (∀𝑥𝐴 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠) ↔ ∀𝑥(𝑥𝐴 → (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠)))
53, 4bitr4i 187 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) ↔ ∀𝑥𝐴 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠))
6 sbim 1965 . . . . . . . . . . 11 ([𝑦 / 𝑥](𝑥𝐴𝑥𝑠) ↔ ([𝑦 / 𝑥]𝑥𝐴 → [𝑦 / 𝑥]𝑥𝑠))
7 clelsb1 2294 . . . . . . . . . . . 12 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
8 clelsb1 2294 . . . . . . . . . . . 12 ([𝑦 / 𝑥]𝑥𝑠𝑦𝑠)
97, 8imbi12i 239 . . . . . . . . . . 11 (([𝑦 / 𝑥]𝑥𝐴 → [𝑦 / 𝑥]𝑥𝑠) ↔ (𝑦𝐴𝑦𝑠))
106, 9bitri 184 . . . . . . . . . 10 ([𝑦 / 𝑥](𝑥𝐴𝑥𝑠) ↔ (𝑦𝐴𝑦𝑠))
1110ralbii 2496 . . . . . . . . 9 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) ↔ ∀𝑦𝑥 (𝑦𝐴𝑦𝑠))
12 ralcom3 2658 . . . . . . . . 9 (∀𝑦𝑥 (𝑦𝐴𝑦𝑠) ↔ ∀𝑦𝐴 (𝑦𝑥𝑦𝑠))
1311, 12bitri 184 . . . . . . . 8 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) ↔ ∀𝑦𝐴 (𝑦𝑥𝑦𝑠))
14 epel 4313 . . . . . . . . . 10 (𝑦 E 𝑥𝑦𝑥)
1514imbi1i 238 . . . . . . . . 9 ((𝑦 E 𝑥𝑦𝑠) ↔ (𝑦𝑥𝑦𝑠))
1615ralbii 2496 . . . . . . . 8 (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) ↔ ∀𝑦𝐴 (𝑦𝑥𝑦𝑠))
1713, 16bitr4i 187 . . . . . . 7 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) ↔ ∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠))
1817imbi1i 238 . . . . . 6 ((∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠) ↔ (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) → 𝑥𝑠))
1918ralbii 2496 . . . . 5 (∀𝑥𝐴 (∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → 𝑥𝑠) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) → 𝑥𝑠))
205, 19bitri 184 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) ↔ ∀𝑥𝐴 (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) → 𝑥𝑠))
21 ax-setind 4557 . . . . 5 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) → ∀𝑥(𝑥𝐴𝑥𝑠))
22 dfss2 3159 . . . . 5 (𝐴𝑠 ↔ ∀𝑥(𝑥𝐴𝑥𝑠))
2321, 22sylibr 134 . . . 4 (∀𝑥(∀𝑦𝑥 [𝑦 / 𝑥](𝑥𝐴𝑥𝑠) → (𝑥𝐴𝑥𝑠)) → 𝐴𝑠)
2420, 23sylbir 135 . . 3 (∀𝑥𝐴 (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠)
25 df-frfor 4352 . . 3 ( FrFor E 𝐴𝑠 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦 E 𝑥𝑦𝑠) → 𝑥𝑠) → 𝐴𝑠))
2624, 25mpbir 146 . 2 FrFor E 𝐴𝑠
271, 26mpgbir 1464 1 E Fr 𝐴
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362  [wsb 1773  wcel 2160  wral 2468  wss 3144   class class class wbr 4021   E cep 4308   FrFor wfrfor 4348   Fr wfr 4349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230  ax-setind 4557
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619  df-br 4022  df-opab 4083  df-eprel 4310  df-frfor 4352  df-frind 4353
This theorem is referenced by:  ordfr  4595  wessep  4598  reg3exmidlemwe  4599
  Copyright terms: Public domain W3C validator