Theorem elima4 35776

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 3501	. 2 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V)
2		xpeq2 5706	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅))
3		xp0 6178	. . . . . . 7 ⊢ (𝐵 × ∅) = ∅
4	2, 3	eqtrdi 2793	. . . . . 6 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅)
5	4	ineq2d 4220	. . . . 5 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅))
6		in0 4395	. . . . 5 ⊢ (𝑅 ∩ ∅) = ∅
7	5, 6	eqtrdi 2793	. . . 4 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅)
8	7	necon3i 2973	. . 3 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅)
9		snnzb 4718	. . 3 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
10	8, 9	sylibr 234	. 2 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V)
11		eleq1 2829	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵)))
12		sneq 4636	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
13	12	xpeq2d 5715	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴}))
14	13	ineq2d 4220	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴})))
15	14	neeq1d 3000	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
16		elin 3967	. . . . . . 7 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})))
17		ancom 460	. . . . . . 7 ⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅))
18		elxp 5708	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})))
19	18	anbi1i 624	. . . . . . 7 ⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
20	16, 17, 19	3bitri 297	. . . . . 6 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
21	20	exbii 1848	. . . . 5 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
22		anass 468	. . . . . . . . 9 ⊢ (((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
23	22	2exbii 1849	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
24		19.41vv 1950	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
25	23, 24	bitr3i 277	. . . . . . 7 ⊢ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
26	25	exbii 1848	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
27		exrot3 2165	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
28	26, 27	bitr3i 277	. . . . 5 ⊢ (∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
29		opex 5469	. . . . . . . . 9 ⊢ ⟨𝑦, 𝑧⟩ ∈ V
30		eleq1 2829	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
31	30	anbi2d 630	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
32	29, 31	ceqsexv 3532	. . . . . . . 8 ⊢ (∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
33	32	exbii 1848	. . . . . . 7 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
34		anass 468	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
35		an12 645	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
36		velsn 4642	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
37	36	anbi1i 624	. . . . . . . . 9 ⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
38	34, 35, 37	3bitri 297	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
39	38	exbii 1848	. . . . . . 7 ⊢ (∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
40		vex 3484	. . . . . . . 8 ⊢ 𝑥 ∈ V
41		opeq2 4874	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑥⟩)
42	41	eleq1d 2826	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
43	42	anbi2d 630	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
44	40, 43	ceqsexv 3532	. . . . . . 7 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
45	33, 39, 44	3bitri 297	. . . . . 6 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
46	45	exbii 1848	. . . . 5 ⊢ (∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
47	21, 28, 46	3bitri 297	. . . 4 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
48		n0 4353	. . . 4 ⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})))
49	40	elima3 6085	. . . 4 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
50	47, 48, 49	3bitr4ri 304	. . 3 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅)
51	11, 15, 50	vtoclbg 3557	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
52	1, 10, 51	pm5.21nii 378	1 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2940  Vcvv 3480   ∩ cin 3950  ∅c0 4333  {csn 4626  ⟨cop 4632   × cxp 5683   “ cima 5688

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-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

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-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by: (None)