copsex2d

Description: Implicit substitution deduction for ordered pairs. (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	copsex2d.xph	$⊢ φ \to \forall x φ$
	copsex2d.yph	$⊢ φ \to \forall y φ$
	copsex2d.xch	$⊢ φ \to Ⅎ x χ$
	copsex2d.ych	$⊢ φ \to Ⅎ y χ$
	copsex2d.exa	$⊢ φ \to A \in U$
	copsex2d.exb	$⊢ φ \to B \in V$
	copsex2d.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
Assertion	copsex2d	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Proof

Step	Hyp	Ref	Expression
1		copsex2d.xph	$⊢ φ \to \forall x φ$
2		copsex2d.yph	$⊢ φ \to \forall y φ$
3		copsex2d.xch	$⊢ φ \to Ⅎ x χ$
4		copsex2d.ych	$⊢ φ \to Ⅎ y χ$
5		copsex2d.exa	$⊢ φ \to A \in U$
6		copsex2d.exb	$⊢ φ \to B \in V$
7		copsex2d.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
8		elisset	$⊢ A \in U \to \exists x x = A$
9	5 8	syl	$⊢ φ \to \exists x x = A$
10		elisset	$⊢ B \in V \to \exists y y = B$
11	6 10	syl	$⊢ φ \to \exists y y = B$
12		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
13		nfe1	$⊢ Ⅎ x \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
14	13	a1i	$⊢ φ \to Ⅎ x \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
15	14 3	nfbid	$⊢ φ \to Ⅎ x (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$
16	15	19.9d	$⊢ φ \to (\exists x (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
17		nfe1	$⊢ Ⅎ y \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
18	17	a1i	$⊢ φ \to Ⅎ y \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
19	1 18	bj-nfexd	$⊢ φ \to Ⅎ y \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)$
20	19 4	nfbid	$⊢ φ \to Ⅎ y (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$
21	20	19.9d	$⊢ φ \to (\exists y (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
22		opeq12	$⊢ (x = A \land y = B) \to ⟨x, y⟩ = ⟨A, B⟩$
23		copsexgw	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (ψ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ))$
24	23	bicomd	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ψ)$
25	24	eqcoms	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ψ)$
26	22 25	syl	$⊢ (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ψ)$
27	26	adantl	$⊢ (φ \land (x = A \land y = B)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ψ)$
28	27 7	bitrd	$⊢ (φ \land (x = A \land y = B)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$
29	28	ex	$⊢ φ \to ((x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
30	2 21 29	bj-exlimd	$⊢ φ \to (\exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
31	1 16 30	bj-exlimd	$⊢ φ \to (\exists x \exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
32	12 31	syl5bir	$⊢ φ \to ((\exists x x = A \land \exists y y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ))$
33	9 11 32	mp2and	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$

Metamath Proof Explorer

Theorem copsex2d

Proof