Theorem bnj110 30182

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 2975	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
2		vex 3176	. . . . . . . 8 ⊢ 𝑧 ∈ V
3		sbcng 3443	. . . . . . . 8 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑))
4	2, 3	ax-mp 5	. . . . . . 7 ⊢ ([𝑧 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑧 / 𝑥]𝜑)
5	4	bicomi 213	. . . . . 6 ⊢ (¬ [𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑥] ¬ 𝜑)
6	5	ralbii 2963	. . . . 5 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ [𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
7	1, 6	bitr3i 265	. . . 4 ⊢ (¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥] ¬ 𝜑)
8		df-rab 2905	. . . . . . 7 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)}
9	8	eleq2i 2680	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
10		df-sbc 3403	. . . . . . 7 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ 𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)})
11		sbcan 3445	. . . . . . . 8 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
12		sbcel1v 3462	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)
13	12	anbi1i 727	. . . . . . . 8 ⊢ (([𝑧 / 𝑥]𝑥 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
14	11, 13	bitri 263	. . . . . . 7 ⊢ ([𝑧 / 𝑥](𝑥 ∈ 𝐴 ∧ ¬ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
15	10, 14	bitr3i 265	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ¬ 𝜑)} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
16	9, 15	bitri 263	. . . . 5 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥] ¬ 𝜑))
17	16	simprbi 479	. . . 4 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → [𝑧 / 𝑥] ¬ 𝜑)
18	7, 17	mprgbir 2911	. . 3 ⊢ ¬ ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑
19		bnj110.1	. . . . . . . . 9 ⊢ 𝐴 ∈ V
20	19	rabex 4740	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V
21	20	biantrur 526	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴))
22		rexnal 2978	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 𝜑)
23		rabn0 3912	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 ¬ 𝜑)
24		ssrab2 3650	. . . . . . . . . 10 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴
25	24	biantrur 526	. . . . . . . . 9 ⊢ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅ ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
26	23, 25	bitr3i 265	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
27	22, 26	bitr3i 265	. . . . . . 7 ⊢ (¬ ∀𝑥 ∈ 𝐴 𝜑 ↔ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅))
28		fri 5000	. . . . . . 7 ⊢ ((({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ∈ V ∧ 𝑅 Fr 𝐴) ∧ ({𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ≠ ∅)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
29	21, 27, 28	syl2anb 495	. . . . . 6 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧)
30		eqid 2610	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} = {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}
31	30	bnj23 30038	. . . . . . 7 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
32		df-ral 2901	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
33	32	sbcbii 3458	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ [𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
34		sbcal 3452	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
35		sbcimg 3444	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))))
36	2, 35	ax-mp 5	. . . . . . . . . . . 12 ⊢ ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)))
37		nfv 1830	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
38	37	sbcgf 3468	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
39	2, 38	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
40		sbcimg 3444	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑)))
41	2, 40	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑))
42		sbcbr2g 4640	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥))
43	2, 42	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅⦋𝑧 / 𝑥⦌𝑥)
44		csbvarg 3955	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ V → ⦋𝑧 / 𝑥⦌𝑥 = 𝑧)
45	2, 44	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ⦋𝑧 / 𝑥⦌𝑥 = 𝑧
46	45	breq2i 4591	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅⦋𝑧 / 𝑥⦌𝑥 ↔ 𝑦𝑅𝑧)
47	43, 46	bitri 263	. . . . . . . . . . . . . . 15 ⊢ ([𝑧 / 𝑥]𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧)
48		nfsbc1v 3422	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
49	48	sbcgf 3468	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ V → ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
50	2, 49	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ([𝑧 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
51	47, 50	imbi12i 339	. . . . . . . . . . . . . 14 ⊢ (([𝑧 / 𝑥]𝑦𝑅𝑥 → [𝑧 / 𝑥][𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
52	41, 51	bitri 263	. . . . . . . . . . . . 13 ⊢ ([𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
53	39, 52	imbi12i 339	. . . . . . . . . . . 12 ⊢ (([𝑧 / 𝑥]𝑦 ∈ 𝐴 → [𝑧 / 𝑥](𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
54	36, 53	bitri 263	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ (𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
55	54	albii 1737	. . . . . . . . . 10 ⊢ (∀𝑦[𝑧 / 𝑥](𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
56	34, 55	bitri 263	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥]∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
57	33, 56	bitri 263	. . . . . . . 8 ⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
58		bnj110.2	. . . . . . . . 9 ⊢ (𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))
59	58	sbcbii 3458	. . . . . . . 8 ⊢ ([𝑧 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → [𝑦 / 𝑥]𝜑))
60		df-ral 2901	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑)))
61	57, 59, 60	3bitr4i 291	. . . . . . 7 ⊢ ([𝑧 / 𝑥]𝜓 ↔ ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑧 → [𝑦 / 𝑥]𝜑))
62	31, 61	sylibr 223	. . . . . 6 ⊢ (∀𝑤 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ¬ 𝑤𝑅𝑧 → [𝑧 / 𝑥]𝜓)
63	29, 62	bnj31 30039	. . . . 5 ⊢ ((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓)
64		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑧(𝜓 → 𝜑)
65		nfsbc1v 3422	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜓
66		nfsbc1v 3422	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑
67	65, 66	nfim 1813	. . . . . . . 8 ⊢ Ⅎ𝑥([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)
68		sbceq1a 3413	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜓 ↔ [𝑧 / 𝑥]𝜓))
69		sbceq1a 3413	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
70	68, 69	imbi12d 333	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝜓 → 𝜑) ↔ ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
71	64, 67, 70	cbvral 3143	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) ↔ ∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
72		elrabi 3328	. . . . . . . . 9 ⊢ (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → 𝑧 ∈ 𝐴)
73	72	imim1i 61	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝐴 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)) → (𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑)))
74	73	ralimi2 2933	. . . . . . 7 ⊢ (∀𝑧 ∈ 𝐴 ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
75	71, 74	sylbi 206	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → ∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑))
76		rexim 2991	. . . . . 6 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑} ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑))
77	75, 76	syl 17	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → 𝜑) → (∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜓 → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑))
78	63, 77	mpan9 485	. . . 4 ⊢ (((𝑅 Fr 𝐴 ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
79	78	an32s 842	. . 3 ⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑) → ∃𝑧 ∈ {𝑥 ∈ 𝐴 ∣ ¬ 𝜑}[𝑧 / 𝑥]𝜑)
80	18, 79	mto 187	. 2 ⊢ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑)
81		iman 439	. 2 ⊢ (((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑) ↔ ¬ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) ∧ ¬ ∀𝑥 ∈ 𝐴 𝜑))
82	80, 81	mpbir 220	1 ⊢ ((𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜑)) → ∀𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173  [wsbc 3402  ⦋csb 3499   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   Fr wfr 4994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-fr 4997

This theorem is referenced by:  bnj157  30183  bnj580  30237  bnj1052  30297  bnj1030  30309  bnj1133  30311