Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem tfrlem1 2949

Description: A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47.

**Assertion**
Ref	Expression
tfrlem1	⊢ (A ∈ On → ((F Fn A ∧ G Fn A) → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x))))

Distinct variable group(s): x,A x,B x,F x,G

**Proof of Theorem tfrlem1**
Step	Hyp	Ref	Expression
1		ssid 1519	. 2 ⊢ A ⊆ A
2		sseq1 1521	. . . . 5 ⊢ (y = A → (y ⊆ A ↔ A ⊆ A))
3		raleq 1324	. . . . . 6 ⊢ (y = A → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) ↔ ∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))
4		raleq 1324	. . . . . 6 ⊢ (y = A → (∀x ∈ y (F ‘x) = (G ‘x) ↔ ∀x ∈ A (F ‘x) = (G ‘x)))
5	3, 4	imbi12d 474	. . . . 5 ⊢ (y = A → ((∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)) ↔ (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x))))
6	2, 5	imbi12d 474	. . . 4 ⊢ (y = A → ((y ⊆ A → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x))) ↔ (A ⊆ A → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x)))))
7	6	imbi2d 464	. . 3 ⊢ (y = A → (((F Fn A ∧ G Fn A) → (y ⊆ A → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)))) ↔ ((F Fn A ∧ G Fn A) → (A ⊆ A → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x))))))
8		sseq1 1521	. . . . . . . 8 ⊢ (y = z → (y ⊆ A ↔ z ⊆ A))
9	8	anbi2d 468	. . . . . . 7 ⊢ (y = z → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) ↔ ((F Fn A ∧ G Fn A) ∧ z ⊆ A)))
10		raleq 1324	. . . . . . 7 ⊢ (y = z → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) ↔ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))
11	9, 10	anbi12d 476	. . . . . 6 ⊢ (y = z → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) ↔ (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))))))
12		raleq 1324	. . . . . 6 ⊢ (y = z → (∀x ∈ y (F ‘x) = (G ‘x) ↔ ∀x ∈ z (F ‘x) = (G ‘x)))
13	11, 12	imbi12d 474	. . . . 5 ⊢ (y = z → (((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x)) ↔ ((((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ z (F ‘x) = (G ‘x))))
14		onelsst 2255	. . . . . . . . . . 11 ⊢ (y ∈ On → (z ∈ y → z ⊆ y))
15		sstr2 1510	. . . . . . . . . . . . 13 ⊢ (z ⊆ y → (y ⊆ A → z ⊆ A))
16	15	anim2d 433	. . . . . . . . . . . 12 ⊢ (z ⊆ y → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) → ((F Fn A ∧ G Fn A) ∧ z ⊆ A)))
17		ax-17 925	. . . . . . . . . . . . 13 ⊢ (z ⊆ y → ∀x z ⊆ y)
18		hbra1 1237	. . . . . . . . . . . . 13 ⊢ (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))))
19		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (z ⊆ y → (x ∈ z → x ∈ y))
20		ra4 1243	. . . . . . . . . . . . . 14 ⊢ (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (x ∈ y → ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))
21	19, 20	syl9 55	. . . . . . . . . . . . 13 ⊢ (z ⊆ y → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (x ∈ z → ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))))))
22	17, 18, 21	r19.21ad 1261	. . . . . . . . . . . 12 ⊢ (z ⊆ y → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))
23	16, 22	anim12d 431	. . . . . . . . . . 11 ⊢ (z ⊆ y → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))))))
24	14, 23	syl6 23	. . . . . . . . . 10 ⊢ (y ∈ On → (z ∈ y → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))))
25	24	com23 32	. . . . . . . . 9 ⊢ (y ∈ On → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → (z ∈ y → (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))))))
26	25	r19.21adv 1262	. . . . . . . 8 ⊢ (y ∈ On → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀z ∈ y (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))))))
27		onelsst 2255	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ On → (x ∈ y → x ⊆ y))
28		sstr2 1510	. . . . . . . . . . . . . . . . . . 19 ⊢ (x ⊆ y → (y ⊆ A → x ⊆ A))
29		cleq12 1113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ((F ‘x) = (G ‘x) ↔ (B ‘(F ↾ x)) = (B ‘(G ↾ x))))
30		fvreseq 2882	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((F Fn A ∧ G Fn A) ∧ x ⊆ A) → ((F ↾ x) = (G ↾ x) ↔ ∀w ∈ x (F ‘w) = (G ‘w)))
31	30	biimpar 325	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((F Fn A ∧ G Fn A) ∧ x ⊆ A) ∧ ∀w ∈ x (F ‘w) = (G ‘w)) → (F ↾ x) = (G ↾ x))
32	31	fveq2d 2836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((F Fn A ∧ G Fn A) ∧ x ⊆ A) ∧ ∀w ∈ x (F ‘w) = (G ‘w)) → (B ‘(F ↾ x)) = (B ‘(G ↾ x)))
33	29, 32	syl5bir 184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ((((F Fn A ∧ G Fn A) ∧ x ⊆ A) ∧ ∀w ∈ x (F ‘w) = (G ‘w)) → (F ‘x) = (G ‘x)))
34	33	exp4c 297	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ((F Fn A ∧ G Fn A) → (x ⊆ A → (∀w ∈ x (F ‘w) = (G ‘w) → (F ‘x) = (G ‘x)))))
35	34	com4l 39	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F Fn A ∧ G Fn A) → (x ⊆ A → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x)))))
36	28, 35	syl9 55	. . . . . . . . . . . . . . . . . 18 ⊢ (x ⊆ y → ((F Fn A ∧ G Fn A) → (y ⊆ A → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x))))))
37	27, 36	syl6 23	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ On → (x ∈ y → ((F Fn A ∧ G Fn A) → (y ⊆ A → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x)))))))
38	37	imp4a 282	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ On → (x ∈ y → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x))))))
39	38	com23 32	. . . . . . . . . . . . . . 15 ⊢ (y ∈ On → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) → (x ∈ y → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x))))))
40	39	imp31 280	. . . . . . . . . . . . . 14 ⊢ (((y ∈ On ∧ ((F Fn A ∧ G Fn A) ∧ y ⊆ A)) ∧ x ∈ y) → (∀w ∈ x (F ‘w) = (G ‘w) → (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x))))
41	40	r19.20dva 1256	. . . . . . . . . . . . 13 ⊢ ((y ∈ On ∧ ((F Fn A ∧ G Fn A) ∧ y ⊆ A)) → (∀x ∈ y ∀w ∈ x (F ‘w) = (G ‘w) → ∀x ∈ y (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x))))
42		r19.20 1251	. . . . . . . . . . . . 13 ⊢ (∀x ∈ y (((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → (F ‘x) = (G ‘x)) → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)))
43	41, 42	syl6 23	. . . . . . . . . . . 12 ⊢ ((y ∈ On ∧ ((F Fn A ∧ G Fn A) ∧ y ⊆ A)) → (∀x ∈ y ∀w ∈ x (F ‘w) = (G ‘w) → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x))))
44		hbra1 1237	. . . . . . . . . . . . 13 ⊢ (∀x ∈ z (F ‘x) = (G ‘x) → ∀x∀x ∈ z (F ‘x) = (G ‘x))
45		ax-17 925	. . . . . . . . . . . . 13 ⊢ (∀w ∈ x (F ‘w) = (G ‘w) → ∀z∀w ∈ x (F ‘w) = (G ‘w))
46		raleq 1324	. . . . . . . . . . . . . 14 ⊢ (z = x → (∀w ∈ z (F ‘w) = (G ‘w) ↔ ∀w ∈ x (F ‘w) = (G ‘w)))
47		fveq2 2832	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (F ‘x) = (F ‘w))
48		fveq2 2832	. . . . . . . . . . . . . . . 16 ⊢ (x = w → (G ‘x) = (G ‘w))
49	47, 48	cleq12d 1115	. . . . . . . . . . . . . . 15 ⊢ (x = w → ((F ‘x) = (G ‘x) ↔ (F ‘w) = (G ‘w)))
50	49	cbvralv 1333	. . . . . . . . . . . . . 14 ⊢ (∀x ∈ z (F ‘x) = (G ‘x) ↔ ∀w ∈ z (F ‘w) = (G ‘w))
51	46, 50	syl5bb 410	. . . . . . . . . . . . 13 ⊢ (z = x → (∀x ∈ z (F ‘x) = (G ‘x) ↔ ∀w ∈ x (F ‘w) = (G ‘w)))
52	44, 45, 51	cbvral 1331	. . . . . . . . . . . 12 ⊢ (∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x) ↔ ∀x ∈ y ∀w ∈ x (F ‘w) = (G ‘w))
53	43, 52	syl5ib 181	. . . . . . . . . . 11 ⊢ ((y ∈ On ∧ ((F Fn A ∧ G Fn A) ∧ y ⊆ A)) → (∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x) → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x))))
54	53	exp 291	. . . . . . . . . 10 ⊢ (y ∈ On → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) → (∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x) → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)))))
55	54	com23 32	. . . . . . . . 9 ⊢ (y ∈ On → (∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x) → (((F Fn A ∧ G Fn A) ∧ y ⊆ A) → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)))))
56	55	imp4a 282	. . . . . . . 8 ⊢ (y ∈ On → (∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x))))
57	26, 56	syl34d 29	. . . . . . 7 ⊢ (y ∈ On → ((∀z ∈ y (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x)) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x)))))
58		pm2.43 57	. . . . . . 7 ⊢ (((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x))) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x)))
59	57, 58	syl6 23	. . . . . 6 ⊢ (y ∈ On → ((∀z ∈ y (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x)) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x))))
60		r19.20 1251	. . . . . 6 ⊢ (∀z ∈ y ((((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ z (F ‘x) = (G ‘x)) → (∀z ∈ y (((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀z ∈ y ∀x ∈ z (F ‘x) = (G ‘x)))
61	59, 60	syl5 22	. . . . 5 ⊢ (y ∈ On → (∀z ∈ y ((((F Fn A ∧ G Fn A) ∧ z ⊆ A) ∧ ∀x ∈ z ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ z (F ‘x) = (G ‘x)) → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x))))
62	13, 61	tfis2 2247	. . . 4 ⊢ (y ∈ On → ((((F Fn A ∧ G Fn A) ∧ y ⊆ A) ∧ ∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x)))) → ∀x ∈ y (F ‘x) = (G ‘x)))
63	62	exp4c 297	. . 3 ⊢ (y ∈ On → ((F Fn A ∧ G Fn A) → (y ⊆ A → (∀x ∈ y ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ y (F ‘x) = (G ‘x)))))
64	7, 63	vtoclga 1387	. 2 ⊢ (A ∈ On → ((F Fn A ∧ G Fn A) → (A ⊆ A → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x)))))
65	1, 64	mpii 45	1 ⊢ (A ∈ On → ((F Fn A ∧ G Fn A) → (∀x ∈ A ((F ‘x) = (B ‘(F ↾ x)) ∧ (G ‘x) = (B ‘(G ↾ x))) → ∀x ∈ A (F ‘x) = (G ‘x))))

Colors of variables: wff set class

Syntax hints: → wi 2 ∧ wa 196 = weq 797 ∈ wel 803 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ⊆ wss 1487 Oncon0 2199 ↾ cres 2412 Fn wfn 2417 ‘cfv 2422

This theorem is referenced by: tfrlem2 2950

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438

metamath.org