Theorem zfregfr 4678

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.

Step	Hyp	Ref	Expression
1		df-frind 4435	. 2 ⊢ ( E Fr 𝐴 ↔ ∀𝑠 FrFor E 𝐴𝑠)
2		bi2.04 248	. . . . . . 7 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) ↔ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠)))
3	2	albii 1519	. . . . . 6 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠)))
4		df-ral 2516	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠)))
5	3, 4	bitr4i 187	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠))
6		sbim 2006	. . . . . . . . . . 11 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 → [𝑦 / 𝑥]𝑥 ∈ 𝑠))
7		clelsb1 2336	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
8		clelsb1 2336	. . . . . . . . . . . 12 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝑠 ↔ 𝑦 ∈ 𝑠)
9	7, 8	imbi12i 239	. . . . . . . . . . 11 ⊢ (([𝑦 / 𝑥]𝑥 ∈ 𝐴 → [𝑦 / 𝑥]𝑥 ∈ 𝑠) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑠))
10	6, 9	bitri 184	. . . . . . . . . 10 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) ↔ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑠))
11	10	ralbii 2539	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) ↔ ∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑠))
12		ralcom3 2702	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝑥 (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝑠) ↔ ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑠))
13	11, 12	bitri 184	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) ↔ ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑠))
14		epel 4395	. . . . . . . . . 10 ⊢ (𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥)
15	14	imbi1i 238	. . . . . . . . 9 ⊢ ((𝑦 E 𝑥 → 𝑦 ∈ 𝑠) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑠))
16	15	ralbii 2539	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) ↔ ∀𝑦 ∈ 𝐴 (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑠))
17	13, 16	bitr4i 187	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) ↔ ∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠))
18	17	imbi1i 238	. . . . . 6 ⊢ ((∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠) ↔ (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠))
19	18	ralbii 2539	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → 𝑥 ∈ 𝑠) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠))
20	5, 19	bitri 184	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠))
21		ax-setind 4641	. . . . 5 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠))
22		ssalel 3216	. . . . 5 ⊢ (𝐴 ⊆ 𝑠 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠))
23	21, 22	sylibr 134	. . . 4 ⊢ (∀𝑥(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠) → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑠)) → 𝐴 ⊆ 𝑠)
24	20, 23	sylbir 135	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠) → 𝐴 ⊆ 𝑠)
25		df-frfor 4434	. . 3 ⊢ ( FrFor E 𝐴𝑠 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦 E 𝑥 → 𝑦 ∈ 𝑠) → 𝑥 ∈ 𝑠) → 𝐴 ⊆ 𝑠))
26	24, 25	mpbir 146	. 2 ⊢ FrFor E 𝐴𝑠
27	1, 26	mpgbir 1502	1 ⊢ E Fr 𝐴

Syntax hints:   → wi 4  ∀wal 1396  [wsb 1810   ∈ wcel 2202  ∀wral 2511   ⊆ wss 3201   class class class wbr 4093   E cep 4390   FrFor wfrfor 4430   Fr wfr 4431

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-setind 4641

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094  df-opab 4156  df-eprel 4392  df-frfor 4434  df-frind 4435

This theorem is referenced by:  ordfr  4679  wessep  4682  reg3exmidlemwe  4683