Definition df-fr 2169

Description: Define a founded relation. For alternate definitions, see dffr2 2171 and dffr3 2620.

Assertion

Ref	Expression
df-fr	⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))

Distinct variable group(s):   x,y,z,R   x,A,y,z

Detailed syntax breakdown of Definition df-fr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wfr 2061	. 2 wff R Fr A
4		vx	. . . . . . 7 set x
5	4	cv 1089	. . . . . 6 class x
6	5, 1	wss 1487	. . . . 5 wff x ⊆ A
7		c0 1707	. . . . . . 7 class ∅
8	5, 7	wceq 1091	. . . . . 6 wff x = ∅
9	8	wn 1	. . . . 5 wff ¬ x = ∅
10	6, 9	wa 196	. . . 4 wff (x ⊆ A ∧ ¬ x = ∅)
11		vz	. . . . . . . . 9 set z
12	11	cv 1089	. . . . . . . 8 class z
13		vy	. . . . . . . . 9 set y
14	13	cv 1089	. . . . . . . 8 class y
15	12, 14, 2	wbr 2054	. . . . . . 7 wff zRy
16	15	wn 1	. . . . . 6 wff ¬ zRy
17	16, 11, 5	wral 1201	. . . . 5 wff ∀z ∈ x ¬ zRy
18	17, 13, 5	wrex 1202	. . . 4 wff ∃y ∈ x ∀z ∈ x ¬ zRy
19	10, 18	wi 2	. . 3 wff ((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy)
20	19, 4	wal 672	. 2 wff ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy)
21	3, 20	wb 127	1 wff (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x ∀z ∈ x ¬ zRy))

This definition is referenced by:  fri 2170  dffr2 2171  freq1 2174  weinxp 2467  f1oweOLD 944

metamath.org