Theorem elima4 33019

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 3512	. 2 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V)
2		xpeq2 5576	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅))
3		xp0 6015	. . . . . . 7 ⊢ (𝐵 × ∅) = ∅
4	2, 3	syl6eq 2872	. . . . . 6 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅)
5	4	ineq2d 4189	. . . . 5 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅))
6		in0 4345	. . . . 5 ⊢ (𝑅 ∩ ∅) = ∅
7	5, 6	syl6eq 2872	. . . 4 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅)
8	7	necon3i 3048	. . 3 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅)
9		snnzb 4654	. . 3 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
10	8, 9	sylibr 236	. 2 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V)
11		eleq1 2900	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵)))
12		sneq 4577	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
13	12	xpeq2d 5585	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴}))
14	13	ineq2d 4189	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴})))
15	14	neeq1d 3075	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
16		elin 4169	. . . . . . 7 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})))
17		ancom 463	. . . . . . 7 ⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅))
18		elxp 5578	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})))
19	18	anbi1i 625	. . . . . . 7 ⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
20	16, 17, 19	3bitri 299	. . . . . 6 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
21	20	exbii 1848	. . . . 5 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
22		anass 471	. . . . . . . . 9 ⊢ (((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
23	22	2exbii 1849	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
24		19.41vv 1951	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
25	23, 24	bitr3i 279	. . . . . . 7 ⊢ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
26	25	exbii 1848	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
27		exrot3 2172	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
28	26, 27	bitr3i 279	. . . . 5 ⊢ (∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
29		opex 5356	. . . . . . . . 9 ⊢ ⟨𝑦, 𝑧⟩ ∈ V
30		eleq1 2900	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
31	30	anbi2d 630	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
32	29, 31	ceqsexv 3541	. . . . . . . 8 ⊢ (∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
33	32	exbii 1848	. . . . . . 7 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
34		anass 471	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
35		an12 643	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
36		velsn 4583	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
37	36	anbi1i 625	. . . . . . . . 9 ⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
38	34, 35, 37	3bitri 299	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
39	38	exbii 1848	. . . . . . 7 ⊢ (∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
40		vex 3497	. . . . . . . 8 ⊢ 𝑥 ∈ V
41		opeq2 4804	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑥⟩)
42	41	eleq1d 2897	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
43	42	anbi2d 630	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
44	40, 43	ceqsexv 3541	. . . . . . 7 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
45	33, 39, 44	3bitri 299	. . . . . 6 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
46	45	exbii 1848	. . . . 5 ⊢ (∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
47	21, 28, 46	3bitri 299	. . . 4 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
48		n0 4310	. . . 4 ⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})))
49	40	elima3 5936	. . . 4 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
50	47, 48, 49	3bitr4ri 306	. . 3 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅)
51	11, 15, 50	vtoclbg 3569	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
52	1, 10, 51	pm5.21nii 382	1 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ∩ cin 3935  ∅c0 4291  {csn 4567  ⟨cop 4573   × cxp 5553   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by: (None)