Theorem elima4 31679

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 3212	. 2 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V)
2		xpeq2 5129	. . . . . . 7 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅))
3		xp0 5552	. . . . . . 7 ⊢ (𝐵 × ∅) = ∅
4	2, 3	syl6eq 2672	. . . . . 6 ⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅)
5	4	ineq2d 3814	. . . . 5 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅))
6		in0 3968	. . . . 5 ⊢ (𝑅 ∩ ∅) = ∅
7	5, 6	syl6eq 2672	. . . 4 ⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅)
8	7	necon3i 2826	. . 3 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅)
9		snnzb 4254	. . 3 ⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅)
10	8, 9	sylibr 224	. 2 ⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V)
11		eleq1 2689	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵)))
12		sneq 4187	. . . . . 6 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
13	12	xpeq2d 5139	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴}))
14	13	ineq2d 3814	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴})))
15	14	neeq1d 2853	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
16		elin 3796	. . . . . . 7 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})))
17		ancom 466	. . . . . . 7 ⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅))
18		elxp 5131	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})))
19	18	anbi1i 731	. . . . . . 7 ⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
20	16, 17, 19	3bitri 286	. . . . . 6 ⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
21	20	exbii 1774	. . . . 5 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
22		anass 681	. . . . . . . . 9 ⊢ (((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
23	22	2exbii 1775	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
24		19.41vv 1915	. . . . . . . 8 ⊢ (∃𝑦∃𝑧((𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
25	23, 24	bitr3i 266	. . . . . . 7 ⊢ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
26	25	exbii 1774	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅))
27		exrot3 2045	. . . . . 6 ⊢ (∃𝑝∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
28	26, 27	bitr3i 266	. . . . 5 ⊢ (∃𝑝(∃𝑦∃𝑧(𝑝 = ⟨𝑦, 𝑧⟩ ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)))
29		opex 4932	. . . . . . . . 9 ⊢ ⟨𝑦, 𝑧⟩ ∈ V
30		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
31	30	anbi2d 740	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝑦, 𝑧⟩ → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
32	29, 31	ceqsexv 3242	. . . . . . . 8 ⊢ (∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
33	32	exbii 1774	. . . . . . 7 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅))
34		anass 681	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
35		an12 838	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
36		velsn 4193	. . . . . . . . . 10 ⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥)
37	36	anbi1i 731	. . . . . . . . 9 ⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
38	34, 35, 37	3bitri 286	. . . . . . . 8 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
39	38	exbii 1774	. . . . . . 7 ⊢ (∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)))
40		vex 3203	. . . . . . . 8 ⊢ 𝑥 ∈ V
41		opeq2 4403	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → ⟨𝑦, 𝑧⟩ = ⟨𝑦, 𝑥⟩)
42	41	eleq1d 2686	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (⟨𝑦, 𝑧⟩ ∈ 𝑅 ↔ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
43	42	anbi2d 740	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅)))
44	40, 43	ceqsexv 3242	. . . . . . 7 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑧⟩ ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
45	33, 39, 44	3bitri 286	. . . . . 6 ⊢ (∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
46	45	exbii 1774	. . . . 5 ⊢ (∃𝑦∃𝑧∃𝑝(𝑝 = ⟨𝑦, 𝑧⟩ ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
47	21, 28, 46	3bitri 286	. . . 4 ⊢ (∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
48		n0 3931	. . . 4 ⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})))
49	40	elima3 5473	. . . 4 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ ⟨𝑦, 𝑥⟩ ∈ 𝑅))
50	47, 48, 49	3bitr4ri 293	. . 3 ⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅)
51	11, 15, 50	vtoclbg 3267	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅))
52	1, 10, 51	pm5.21nii 368	1 ⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  Vcvv 3200   ∩ cin 3573  ∅c0 3915  {csn 4177  ⟨cop 4183   × cxp 5112   “ cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by: (None)