copsex2dv

Description: Implicit substitution deduction for ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025)

	Ref	Expression
Hypotheses	copsex2dv.a	$⊢ φ \to A \in U$
	copsex2dv.b	$⊢ φ \to B \in V$
	copsex2dv.1	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	copsex2dv	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Step	Hyp	Ref	Expression
1		copsex2dv.a	$⊢ φ \to A \in U$
2		copsex2dv.b	$⊢ φ \to B \in V$
3		copsex2dv.1	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
4	3	ex	$⊢ φ \to ((x = A \land y = B) \to (ψ \leftrightarrow χ))$
5	4	alrimivv	$⊢ φ \to \forall x \forall y ((x = A \land y = B) \to (ψ \leftrightarrow χ))$
6		copsex2t	$⊢ (\forall x \forall y ((x = A \land y = B) \to (ψ \leftrightarrow χ)) \land (A \in U \land B \in V)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$
7	5 1 2 6	syl12anc	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Metamath Proof Explorer