Theorem bnj110 34894

Description: Well-founded induction restricted to a set (𝐴 ∈ V). The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj110.1	⊢ 𝐴 ∈ V
bnj110.2	⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))

Assertion

Ref	Expression
bnj110	⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝑅,𝑦   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦)

Proof of Theorem bnj110

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ralnex 3063	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
2		sbcng 3818	. . . . . . . 8 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑))
3	2	elv 3469	. . . . . . 7 ⊢ ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑)
4	3	bicomi 224	. . . . . 6 ⊢ (¬ [𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥] ¬ 𝜑)
5	4	ralbii 3083	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
6	1, 5	bitr3i 277	. . . 4 ⊢ (¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
7		df-rab 3421	. . . . . . 7 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}
8	7	eleq2i 2827	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
9		df-sbc 3771	. . . . . . 7 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
10		sbcan 3820	. . . . . . . 8 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
11		sbcel1v 3836	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)
12	11	anbi1i 624	. . . . . . . 8 ⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
13	10, 12	bitri 275	. . . . . . 7 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
14	9, 13	bitr3i 277	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
15	8, 14	bitri 275	. . . . 5 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
16	15	simprbi 496	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → [𝑧 / 𝑥] ¬ 𝜑)
17	6, 16	mprgbir 3059	. . 3 ⊢ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑
18		bnj110.1	. . . . . . . . 9 ⊢ 𝐴 ∈ V
19	18	rabex 5314	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V
20	19	biantrur 530	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴))
21		rexnal 3090	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
22		rabn0 4369	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
23		ssrab2 4060	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴
24	23	biantrur 530	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
25	22, 24	bitr3i 277	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
26	21, 25	bitr3i 277	. . . . . . 7 ⊢ (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
27		fri 5616	. . . . . . 7 ⊢ ((({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
28	20, 26, 27	syl2anb 598	. . . . . 6 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
29		eqid 2736	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
30	29	bnj23 34754	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
31		df-ral 3053	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
32	31	sbcbii 3827	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
33		sbcal 3830	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
34		sbcimg 3819	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))))
35	34	elv 3469	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
36		vex 3468	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
37		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
38	36, 37	sbcgfi 3844	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
39		sbcimg 3819	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑)))
40	39	elv 3469	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑))
41		sbcbr2g 5182	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥))
42	41	elv 3469	. . . . . . . . . . . . . . . 16 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥)
43	36	csbvargi 4415	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝑧 / 𝑥⦌𝑥 = 𝑧
44	43	breq2i 5132	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅⦋𝑧 / 𝑥⦌𝑥 ↔ 𝑦𝑅𝑧)
45	42, 44	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧)
46		nfsbc1v 3790	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
47	36, 46	sbcgfi 3844	. . . . . . . . . . . . . . 15 ⊢ ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
48	45, 47	imbi12i 350	. . . . . . . . . . . . . 14 ⊢ (([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
49	40, 48	bitri 275	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
50	38, 49	imbi12i 350	. . . . . . . . . . . 12 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
51	35, 50	bitri 275	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
52	51	albii 1819	. . . . . . . . . 10 ⊢ (∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
53	33, 52	bitri 275	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
54	32, 53	bitri 275	. . . . . . . 8 ⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
55		bnj110.2	. . . . . . . . 9 ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))
56	55	sbcbii 3827	. . . . . . . 8 ⊢ ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))
57		df-ral 3053	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
58	54, 56, 57	3bitr4i 303	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
59	30, 58	sylibr 234	. . . . . 6 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → [𝑧 / 𝑥]𝜓)
60	28, 59	bnj31 34755	. . . . 5 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓)
61		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑧(𝜓 → 𝜑)
62		nfsbc1v 3790	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
63		nfsbc1v 3790	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑
64	62, 63	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)
65		sbceq1a 3781	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓))
66		sbceq1a 3781	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
67	65, 66	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝜓 → 𝜑) ↔ ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
68	61, 64, 67	cbvralw 3290	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ↔ ∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
69		elrabi 3671	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → 𝑧 ∈ 𝐴)
70	69	imim1i 63	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) → (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
71	70	ralimi2 3069	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
72	68, 71	sylbi 217	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
73		rexim 3078	. . . . . 6 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑))
74	72, 73	syl 17	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑))
75	60, 74	mpan9 506	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
76	75	an32s 652	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
77	17, 76	mto 197	. 2 ⊢ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑)
78		iman 401	. 2 ⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) ↔ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑))
79	77, 78	mpbir 231	1 ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420  Vcvv 3464  [wsbc 3770  ⦋csb 3879   ⊆ wss 3931  ∅c0 4313   class class class wbr 5124   Fr wfr 5608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-fr 5611

This theorem is referenced by:  bnj157  34895  bnj580  34949  bnj1052  35011  bnj1030  35023  bnj1133  35025