opreuopreu

Description: There is a unique ordered pair fulfilling a wff iff its components fulfil a corresponding wff. (Contributed by AV, 2-Jul-2023)

		Ref	Expression
	Hypothesis	opreuopreu.a	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (ψ \leftrightarrow φ)$
	Assertion	opreuopreu	$⊢ \exists! p \in (A \times B) φ \leftrightarrow \exists! p \in (A \times B) \exists a \exists b (p = ⟨a, b⟩ \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		opreuopreu.a	$⊢ (a = 1^{st} (p) \land b = 2^{nd} (p)) \to (ψ \leftrightarrow φ)$
2		elxpi	$⊢ p \in (A \times B) \to \exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in B))$
3		simprl	$⊢ (φ \land (p = ⟨a, b⟩ \land (a \in A \land b \in B))) \to p = ⟨a, b⟩$
4		vex	$⊢ a \in V$
5		vex	$⊢ b \in V$
6	4 5	op1st	$⊢ 1^{st} (⟨a, b⟩) = a$
7	6	eqcomi	$⊢ a = 1^{st} (⟨a, b⟩)$
8	4 5	op2nd	$⊢ 2^{nd} (⟨a, b⟩) = b$
9	8	eqcomi	$⊢ b = 2^{nd} (⟨a, b⟩)$
10	7 9	pm3.2i	$⊢ (a = 1^{st} (⟨a, b⟩) \land b = 2^{nd} (⟨a, b⟩))$
11		fveq2	$⊢ p = ⟨a, b⟩ \to 1^{st} (p) = 1^{st} (⟨a, b⟩)$
12	11	eqeq2d	$⊢ p = ⟨a, b⟩ \to (a = 1^{st} (p) \leftrightarrow a = 1^{st} (⟨a, b⟩))$
13		fveq2	$⊢ p = ⟨a, b⟩ \to 2^{nd} (p) = 2^{nd} (⟨a, b⟩)$
14	13	eqeq2d	$⊢ p = ⟨a, b⟩ \to (b = 2^{nd} (p) \leftrightarrow b = 2^{nd} (⟨a, b⟩))$
15	12 14	anbi12d	$⊢ p = ⟨a, b⟩ \to ((a = 1^{st} (p) \land b = 2^{nd} (p)) \leftrightarrow (a = 1^{st} (⟨a, b⟩) \land b = 2^{nd} (⟨a, b⟩)))$
16	10 15	mpbiri	$⊢ p = ⟨a, b⟩ \to (a = 1^{st} (p) \land b = 2^{nd} (p))$
17	16 1	syl	$⊢ p = ⟨a, b⟩ \to (ψ \leftrightarrow φ)$
18	17	biimprd	$⊢ p = ⟨a, b⟩ \to (φ \to ψ)$
19	18	adantr	$⊢ (p = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (φ \to ψ)$
20	19	impcom	$⊢ (φ \land (p = ⟨a, b⟩ \land (a \in A \land b \in B))) \to ψ$
21	3 20	jca	$⊢ (φ \land (p = ⟨a, b⟩ \land (a \in A \land b \in B))) \to (p = ⟨a, b⟩ \land ψ)$
22	21	ex	$⊢ φ \to ((p = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (p = ⟨a, b⟩ \land ψ))$
23	22	2eximdv	$⊢ φ \to (\exists a \exists b (p = ⟨a, b⟩ \land (a \in A \land b \in B)) \to \exists a \exists b (p = ⟨a, b⟩ \land ψ))$
24	2 23	syl5com	$⊢ p \in (A \times B) \to (φ \to \exists a \exists b (p = ⟨a, b⟩ \land ψ))$
25	17	biimpa	$⊢ (p = ⟨a, b⟩ \land ψ) \to φ$
26	25	a1i	$⊢ p \in (A \times B) \to ((p = ⟨a, b⟩ \land ψ) \to φ)$
27	26	exlimdvv	$⊢ p \in (A \times B) \to (\exists a \exists b (p = ⟨a, b⟩ \land ψ) \to φ)$
28	24 27	impbid	$⊢ p \in (A \times B) \to (φ \leftrightarrow \exists a \exists b (p = ⟨a, b⟩ \land ψ))$
29	28	reubiia	$⊢ \exists! p \in (A \times B) φ \leftrightarrow \exists! p \in (A \times B) \exists a \exists b (p = ⟨a, b⟩ \land ψ)$

Metamath Proof Explorer

Theorem opreuopreu

Proof