copsex2t

Description: Closed theorem form of copsex2g . (Contributed by NM, 17-Feb-2013)

		Ref	Expression
	Assertion	copsex2t	$⊢ (\forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \land (A \in V \land B \in W)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$⊢ Ⅎ x \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ))$
2		nfe1	$⊢ Ⅎ x \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
3		nfv	$⊢ Ⅎ x ψ$
4	2 3	nfbi	$⊢ Ⅎ x (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
5		nfa2	$⊢ Ⅎ y \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ))$
6		nfe1	$⊢ Ⅎ y \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
7	6	nfex	$⊢ Ⅎ y \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ)$
8		nfv	$⊢ Ⅎ y ψ$
9	7 8	nfbi	$⊢ Ⅎ y (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
10		opeq12	$⊢ (x = A \land y = B) \to ⟨x, y⟩ = ⟨A, B⟩$
11		copsexgw	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
12	11	eqcoms	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
13	10 12	syl	$⊢ (x = A \land y = B) \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
14	13	adantl	$⊢ (\forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \land (x = A \land y = B)) \to (φ \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ))$
15		2sp	$⊢ \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \to ((x = A \land y = B) \to (φ \leftrightarrow ψ))$
16	15	imp	$⊢ (\forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \land (x = A \land y = B)) \to (φ \leftrightarrow ψ)$
17	14 16	bitr3d	$⊢ (\forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \land (x = A \land y = B)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$
18	17	ex	$⊢ \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \to ((x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ))$
19	5 9 18	exlimd	$⊢ \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \to (\exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ))$
20	1 4 19	exlimd	$⊢ \forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \to (\exists x \exists y (x = A \land y = B) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ))$
21		elisset	$⊢ A \in V \to \exists x x = A$
22		elisset	$⊢ B \in W \to \exists y y = B$
23	21 22	anim12i	$⊢ (A \in V \land B \in W) \to (\exists x x = A \land \exists y y = B)$
24		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
25	23 24	sylibr	$⊢ (A \in V \land B \in W) \to \exists x \exists y (x = A \land y = B)$
26	20 25	impel	$⊢ (\forall x \forall y ((x = A \land y = B) \to (φ \leftrightarrow ψ)) \land (A \in V \land B \in W)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem copsex2t

Proof