elima4

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

		Ref	Expression
	Assertion	elima4	$⊢ A \in R [B] \leftrightarrow R \cap (B \times \{A\}) \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in R [B] \to A \in V$
2		xpeq2	$⊢ \{A\} = \emptyset \to B \times \{A\} = B \times \emptyset$
3		xp0	$⊢ B \times \emptyset = \emptyset$
4	2 3	eqtrdi	$⊢ \{A\} = \emptyset \to B \times \{A\} = \emptyset$
5	4	ineq2d	$⊢ \{A\} = \emptyset \to R \cap (B \times \{A\}) = R \cap \emptyset$
6		in0	$⊢ R \cap \emptyset = \emptyset$
7	5 6	eqtrdi	$⊢ \{A\} = \emptyset \to R \cap (B \times \{A\}) = \emptyset$
8	7	necon3i	$⊢ R \cap (B \times \{A\}) \neq \emptyset \to \{A\} \neq \emptyset$
9		snnzb	$⊢ A \in V \leftrightarrow \{A\} \neq \emptyset$
10	8 9	sylibr	$⊢ R \cap (B \times \{A\}) \neq \emptyset \to A \in V$
11		eleq1	$⊢ x = A \to (x \in R [B] \leftrightarrow A \in R [B])$
12		sneq	$⊢ x = A \to \{x\} = \{A\}$
13	12	xpeq2d	$⊢ x = A \to B \times \{x\} = B \times \{A\}$
14	13	ineq2d	$⊢ x = A \to R \cap (B \times \{x\}) = R \cap (B \times \{A\})$
15	14	neeq1d	$⊢ x = A \to (R \cap (B \times \{x\}) \neq \emptyset \leftrightarrow R \cap (B \times \{A\}) \neq \emptyset)$
16		elin	$⊢ p \in (R \cap (B \times \{x\})) \leftrightarrow (p \in R \land p \in (B \times \{x\}))$
17		ancom	$⊢ (p \in R \land p \in (B \times \{x\})) \leftrightarrow (p \in (B \times \{x\}) \land p \in R)$
18		elxp	$⊢ p \in (B \times \{x\}) \leftrightarrow \exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\}))$
19	18	anbi1i	$⊢ (p \in (B \times \{x\}) \land p \in R) \leftrightarrow (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
20	16 17 19	3bitri	$⊢ p \in (R \cap (B \times \{x\})) \leftrightarrow (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
21	20	exbii	$⊢ \exists p p \in (R \cap (B \times \{x\})) \leftrightarrow \exists p (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
22		anass	$⊢ ((p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R) \leftrightarrow (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R))$
23	22	2exbii	$⊢ \exists y \exists z ((p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R) \leftrightarrow \exists y \exists z (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R))$
24		19.41vv	$⊢ \exists y \exists z ((p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R) \leftrightarrow (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
25	23 24	bitr3i	$⊢ \exists y \exists z (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
26	25	exbii	$⊢ \exists p \exists y \exists z (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow \exists p (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R)$
27		exrot3	$⊢ \exists p \exists y \exists z (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow \exists y \exists z \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R))$
28	26 27	bitr3i	$⊢ \exists p (\exists y \exists z (p = ⟨y, z⟩ \land (y \in B \land z \in \{x\})) \land p \in R) \leftrightarrow \exists y \exists z \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R))$
29		opex	$⊢ ⟨y, z⟩ \in V$
30		eleq1	$⊢ p = ⟨y, z⟩ \to (p \in R \leftrightarrow ⟨y, z⟩ \in R)$
31	30	anbi2d	$⊢ p = ⟨y, z⟩ \to (((y \in B \land z \in \{x\}) \land p \in R) \leftrightarrow ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R))$
32	29 31	ceqsexv	$⊢ \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R)$
33	32	exbii	$⊢ \exists z \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow \exists z ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R)$
34		anass	$⊢ ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R) \leftrightarrow (y \in B \land (z \in \{x\} \land ⟨y, z⟩ \in R))$
35		an12	$⊢ (y \in B \land (z \in \{x\} \land ⟨y, z⟩ \in R)) \leftrightarrow (z \in \{x\} \land (y \in B \land ⟨y, z⟩ \in R))$
36		velsn	$⊢ z \in \{x\} \leftrightarrow z = x$
37	36	anbi1i	$⊢ (z \in \{x\} \land (y \in B \land ⟨y, z⟩ \in R)) \leftrightarrow (z = x \land (y \in B \land ⟨y, z⟩ \in R))$
38	34 35 37	3bitri	$⊢ ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R) \leftrightarrow (z = x \land (y \in B \land ⟨y, z⟩ \in R))$
39	38	exbii	$⊢ \exists z ((y \in B \land z \in \{x\}) \land ⟨y, z⟩ \in R) \leftrightarrow \exists z (z = x \land (y \in B \land ⟨y, z⟩ \in R))$
40		vex	$⊢ x \in V$
41		opeq2	$⊢ z = x \to ⟨y, z⟩ = ⟨y, x⟩$
42	41	eleq1d	$⊢ z = x \to (⟨y, z⟩ \in R \leftrightarrow ⟨y, x⟩ \in R)$
43	42	anbi2d	$⊢ z = x \to ((y \in B \land ⟨y, z⟩ \in R) \leftrightarrow (y \in B \land ⟨y, x⟩ \in R))$
44	40 43	ceqsexv	$⊢ \exists z (z = x \land (y \in B \land ⟨y, z⟩ \in R)) \leftrightarrow (y \in B \land ⟨y, x⟩ \in R)$
45	33 39 44	3bitri	$⊢ \exists z \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow (y \in B \land ⟨y, x⟩ \in R)$
46	45	exbii	$⊢ \exists y \exists z \exists p (p = ⟨y, z⟩ \land ((y \in B \land z \in \{x\}) \land p \in R)) \leftrightarrow \exists y (y \in B \land ⟨y, x⟩ \in R)$
47	21 28 46	3bitri	$⊢ \exists p p \in (R \cap (B \times \{x\})) \leftrightarrow \exists y (y \in B \land ⟨y, x⟩ \in R)$
48		n0	$⊢ R \cap (B \times \{x\}) \neq \emptyset \leftrightarrow \exists p p \in (R \cap (B \times \{x\}))$
49	40	elima3	$⊢ x \in R [B] \leftrightarrow \exists y (y \in B \land ⟨y, x⟩ \in R)$
50	47 48 49	3bitr4ri	$⊢ x \in R [B] \leftrightarrow R \cap (B \times \{x\}) \neq \emptyset$
51	11 15 50	vtoclbg	$⊢ A \in V \to (A \in R [B] \leftrightarrow R \cap (B \times \{A\}) \neq \emptyset)$
52	1 10 51	pm5.21nii	$⊢ A \in R [B] \leftrightarrow R \cap (B \times \{A\}) \neq \emptyset$

Metamath Proof Explorer

Theorem elima4

Proof