Metamath Proof Explorer

Theorem nqerrel

Description: Any member of ( N. X. N. ) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	nqerrel	$⊢ A \in (𝑵 \times 𝑵) \to A ~_{𝑸} /_{𝑸} (A)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ /_{𝑸} (A) = /_{𝑸} (A)$
2		nqerf	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸$
3		ffn	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸 \to /_{𝑸} Fn (𝑵 \times 𝑵)$
4	2 3	ax-mp	$⊢ /_{𝑸} Fn (𝑵 \times 𝑵)$
5		fnbrfvb	$⊢ (/_{𝑸} Fn (𝑵 \times 𝑵) \land A \in (𝑵 \times 𝑵)) \to (/_{𝑸} (A) = /_{𝑸} (A) \leftrightarrow A /_{𝑸} /_{𝑸} (A))$
6	4 5	mpan	$⊢ A \in (𝑵 \times 𝑵) \to (/_{𝑸} (A) = /_{𝑸} (A) \leftrightarrow A /_{𝑸} /_{𝑸} (A))$
7	1 6	mpbii	$⊢ A \in (𝑵 \times 𝑵) \to A /_{𝑸} /_{𝑸} (A)$
8		df-erq	$⊢ /_{𝑸} = ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)$
9		inss1	$⊢ ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸) \subseteq ~_{𝑸}$
10	8 9	eqsstri	$⊢ /_{𝑸} \subseteq ~_{𝑸}$
11	10	ssbri	$⊢ A /_{𝑸} /_{𝑸} (A) \to A ~_{𝑸} /_{𝑸} (A)$
12	7 11	syl	$⊢ A \in (𝑵 \times 𝑵) \to A ~_{𝑸} /_{𝑸} (A)$