Theorem elima4 36305

Description: Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)

Assertion

Ref	Expression
elima4	⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

Proof of Theorem elima4

Dummy variables 𝑥 𝑝 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3478	. 2 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V)
2		xpeq2 5684	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅))
3		xp0 5763	. . . . . . 7 ⊢ (𝐵 × ∅) = ∅
4	2, 3	eqtrdi 2816	. . . . . 6 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅)
5	4	ineq2d 4173	. . . . 5 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅))
6		in0 4352	. . . . 5 ⊢ (𝑅 ∩ ∅) = ∅
7	5, 6	eqtrdi 2816	. . . 4 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅)
8	7	necon3i 2992	. . 3 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅)
9		snnzb 4686	. . 3 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
10	8, 9	sylibr 237	. 2 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V)
11		eleq1 2853	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵)))
12		sneq 4601	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
13	12	xpeq2d 5693	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴}))
14	13	ineq2d 4173	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴})))
15	14	neeq1d 3019	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
16		elin 3922	. . . . . . 7 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})))
17		ancom 466	. . . . . . 7 ⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅))
18		elxp 5686	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})))
19	18	anbi1i 636	. . . . . . 7 ⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
20	16, 17, 19	3bitri 300	. . . . . 6 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
21	20	exbii 1881	. . . . 5 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
22		anass 474	. . . . . . . . 9 ⊢ (((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
23	22	2exbii 1882	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
24		19.41vv 1983	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
25	23, 24	bitr3i 280	. . . . . . 7 ⊢ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
26	25	exbii 1881	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
27		exrot3 2203	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
28	26, 27	bitr3i 280	. . . . 5 ⊢ (∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
29		opex 5447	. . . . . . . . 9 ⊢ ⟨𝑦, 𝑧⟩ ∈ V
30		eleq1 2853	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
31	30	anbi2d 642	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
32	29, 31	ceqsexv 3505	. . . . . . . 8 ⊢ (∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
33	32	exbii 1881	. . . . . . 7 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
34		anass 474	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
35		an12 658	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
36		velsn 4607	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
37	36	anbi1i 636	. . . . . . . . 9 ⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
38	34, 35, 37	3bitri 300	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
39	38	exbii 1881	. . . . . . 7 ⊢ (∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
40		vex 3461	. . . . . . . 8 ⊢ 𝑥 ∈ V
41		opeq2 4841	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑥⟩)
42	41	eleq1d 2850	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
43	42	anbi2d 642	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
44	40, 43	ceqsexv 3505	. . . . . . 7 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
45	33, 39, 44	3bitri 300	. . . . . 6 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
46	45	exbii 1881	. . . . 5 ⊢ (∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
47	21, 28, 46	3bitri 300	. . . 4 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
48		n0 4307	. . . 4 ⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})))
49	40	elima3 6071	. . . 4 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
50	47, 48, 49	3bitr4ri 307	. . 3 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅)
51	11, 15, 50	vtoclbg 3526	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
52	1, 10, 51	pm5.21nii 381	1 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146   ≠ wne 2960  Vcvv 3457   ∩ cin 3905  ∅c0 4286  {csn 4591  ⟨cop 4597   × cxp 5661   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-11 2195  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by: (None)