Theorem bnj110 34872

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 3072	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
2		sbcng 3836	. . . . . . . 8 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑))
3	2	elv 3485	. . . . . . 7 ⊢ ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑)
4	3	bicomi 224	. . . . . 6 ⊢ (¬ [𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥] ¬ 𝜑)
5	4	ralbii 3093	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
6	1, 5	bitr3i 277	. . . 4 ⊢ (¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
7		df-rab 3437	. . . . . . 7 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}
8	7	eleq2i 2833	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
9		df-sbc 3789	. . . . . . 7 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
10		sbcan 3838	. . . . . . . 8 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
11		sbcel1v 3856	. . . . . . . . 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 3068	. . 3 ⊢ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑
18		bnj110.1	. . . . . . . . 9 ⊢ 𝐴 ∈ V
19	18	rabex 5339	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V
20	19	biantrur 530	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴))
21		rexnal 3100	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
22		rabn0 4389	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
23		ssrab2 4080	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴
24	23	biantrur 530	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
25	22, 24	bitr3i 277	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
26	21, 25	bitr3i 277	. . . . . . 7 ⊢ (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
27		fri 5642	. . . . . . 7 ⊢ ((({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
28	20, 26, 27	syl2anb 598	. . . . . 6 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
29		eqid 2737	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
30	29	bnj23 34732	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
31		df-ral 3062	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
32	31	sbcbii 3846	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
33		sbcal 3849	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
34		sbcimg 3837	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))))
35	34	elv 3485	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
36		vex 3484	. . . . . . . . . . . . . 14 ⊢ 𝑧 ∈ V
37		nfv 1914	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
38	36, 37	sbcgfi 3864	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
39		sbcimg 3837	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑)))
40	39	elv 3485	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑))
41		sbcbr2g 5201	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥))
42	41	elv 3485	. . . . . . . . . . . . . . . 16 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥)
43	36	csbvargi 4435	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝑧 / 𝑥⦌𝑥 = 𝑧
44	43	breq2i 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅⦋𝑧 / 𝑥⦌𝑥 ↔ 𝑦𝑅𝑧)
45	42, 44	bitri 275	. . . . . . . . . . . . . . 15 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧)
46		nfsbc1v 3808	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
47	36, 46	sbcgfi 3864	. . . . . . . . . . . . . . 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 3846	. . . . . . . 8 ⊢ ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))
57		df-ral 3062	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
58	54, 56, 57	3bitr4i 303	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
59	30, 58	sylibr 234	. . . . . 6 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → [𝑧 / 𝑥]𝜓)
60	28, 59	bnj31 34733	. . . . 5 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓)
61		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑧(𝜓 → 𝜑)
62		nfsbc1v 3808	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
63		nfsbc1v 3808	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑
64	62, 63	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)
65		sbceq1a 3799	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓))
66		sbceq1a 3799	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
67	65, 66	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝜓 → 𝜑) ↔ ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
68	61, 64, 67	cbvralw 3306	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ↔ ∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
69		elrabi 3687	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → 𝑧 ∈ 𝐴)
70	69	imim1i 63	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) → (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
71	70	ralimi2 3078	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
72	68, 71	sylbi 217	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
73		rexim 3087	. . . . . 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 2108  {cab 2714   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3436  Vcvv 3480  [wsbc 3788  ⦋csb 3899   ⊆ wss 3951  ∅c0 4333   class class class wbr 5143   Fr wfr 5634

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-fr 5637

This theorem is referenced by:  bnj157  34873  bnj580  34927  bnj1052  34989  bnj1030  35001  bnj1133  35003