Theorem elima4 33656

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 3440	. 2 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V)
2		xpeq2 5601	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅))
3		xp0 6050	. . . . . . 7 ⊢ (𝐵 × ∅) = ∅
4	2, 3	eqtrdi 2795	. . . . . 6 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅)
5	4	ineq2d 4143	. . . . 5 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅))
6		in0 4322	. . . . 5 ⊢ (𝑅 ∩ ∅) = ∅
7	5, 6	eqtrdi 2795	. . . 4 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅)
8	7	necon3i 2975	. . 3 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅)
9		snnzb 4651	. . 3 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
10	8, 9	sylibr 233	. 2 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V)
11		eleq1 2826	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵)))
12		sneq 4568	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
13	12	xpeq2d 5610	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴}))
14	13	ineq2d 4143	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴})))
15	14	neeq1d 3002	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
16		elin 3899	. . . . . . 7 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})))
17		ancom 460	. . . . . . 7 ⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅))
18		elxp 5603	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})))
19	18	anbi1i 623	. . . . . . 7 ⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
20	16, 17, 19	3bitri 296	. . . . . 6 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
21	20	exbii 1851	. . . . 5 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
22		anass 468	. . . . . . . . 9 ⊢ (((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
23	22	2exbii 1852	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
24		19.41vv 1955	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
25	23, 24	bitr3i 276	. . . . . . 7 ⊢ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
26	25	exbii 1851	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
27		exrot3 2167	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
28	26, 27	bitr3i 276	. . . . 5 ⊢ (∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
29		opex 5373	. . . . . . . . 9 ⊢ ⟨𝑦, 𝑧⟩ ∈ V
30		eleq1 2826	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
31	30	anbi2d 628	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
32	29, 31	ceqsexv 3469	. . . . . . . 8 ⊢ (∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
33	32	exbii 1851	. . . . . . 7 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
34		anass 468	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
35		an12 641	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
36		velsn 4574	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
37	36	anbi1i 623	. . . . . . . . 9 ⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
38	34, 35, 37	3bitri 296	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
39	38	exbii 1851	. . . . . . 7 ⊢ (∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
40		vex 3426	. . . . . . . 8 ⊢ 𝑥 ∈ V
41		opeq2 4802	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑥⟩)
42	41	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
43	42	anbi2d 628	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
44	40, 43	ceqsexv 3469	. . . . . . 7 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
45	33, 39, 44	3bitri 296	. . . . . 6 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
46	45	exbii 1851	. . . . 5 ⊢ (∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
47	21, 28, 46	3bitri 296	. . . 4 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
48		n0 4277	. . . 4 ⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})))
49	40	elima3 5965	. . . 4 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
50	47, 48, 49	3bitr4ri 303	. . 3 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅)
51	11, 15, 50	vtoclbg 3497	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
52	1, 10, 51	pm5.21nii 379	1 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108   ≠ wne 2942  Vcvv 3422   ∩ cin 3882  ∅c0 4253  {csn 4558  ⟨cop 4564   × cxp 5578   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by: (None)