copsex2b

Description: Biconditional form of copsex2d . TODO: prove a relative version, that is, with E. x e. V E. y e. W ... ( A e. V /\ B e. W ) . (Contributed by BJ, 27-Dec-2023)

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

Proof

Step	Hyp	Ref	Expression
1		copsex2b.xph	$⊢ φ \to \forall x φ$
2		copsex2b.yph	$⊢ φ \to \forall y φ$
3		copsex2b.xch	$⊢ φ \to Ⅎ x χ$
4		copsex2b.ych	$⊢ φ \to Ⅎ y χ$
5		copsex2b.is	$⊢ (φ \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
6		eqcom	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = ⟨A, B⟩$
7		vex	$⊢ x \in V$
8		vex	$⊢ y \in V$
9	7 8	opth	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow (x = A \land y = B)$
10	6 9	bitri	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow (x = A \land y = B)$
11		eqvisset	$⊢ x = A \to A \in V$
12		eqvisset	$⊢ y = B \to B \in V$
13	11 12	anim12i	$⊢ (x = A \land y = B) \to (A \in V \land B \in V)$
14	10 13	sylbi	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \to (A \in V \land B \in V)$
15	14	adantr	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \to (A \in V \land B \in V)$
16	15	exlimivv	$⊢ \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \to (A \in V \land B \in V)$
17	16	anim2i	$⊢ (φ \land \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ)) \to (φ \land (A \in V \land B \in V))$
18		simpl	$⊢ ((A \in V \land B \in V) \land χ) \to (A \in V \land B \in V)$
19	18	anim2i	$⊢ (φ \land ((A \in V \land B \in V) \land χ)) \to (φ \land (A \in V \land B \in V))$
20		ax-5	$⊢ (A \in V \land B \in V) \to \forall x (A \in V \land B \in V)$
21	1 20	hban	$⊢ (φ \land (A \in V \land B \in V)) \to \forall x (φ \land (A \in V \land B \in V))$
22		ax-5	$⊢ (A \in V \land B \in V) \to \forall y (A \in V \land B \in V)$
23	2 22	hban	$⊢ (φ \land (A \in V \land B \in V)) \to \forall y (φ \land (A \in V \land B \in V))$
24	3	adantr	$⊢ (φ \land (A \in V \land B \in V)) \to Ⅎ x χ$
25	4	adantr	$⊢ (φ \land (A \in V \land B \in V)) \to Ⅎ y χ$
26		simprl	$⊢ (φ \land (A \in V \land B \in V)) \to A \in V$
27		simprr	$⊢ (φ \land (A \in V \land B \in V)) \to B \in V$
28	5	adantlr	$⊢ ((φ \land (A \in V \land B \in V)) \land (x = A \land y = B)) \to (ψ \leftrightarrow χ)$
29	21 23 24 25 26 27 28	copsex2d	$⊢ (φ \land (A \in V \land B \in V)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow χ)$
30		ibar	$⊢ (A \in V \land B \in V) \to (χ \leftrightarrow ((A \in V \land B \in V) \land χ))$
31	30	adantl	$⊢ (φ \land (A \in V \land B \in V)) \to (χ \leftrightarrow ((A \in V \land B \in V) \land χ))$
32	29 31	bitrd	$⊢ (φ \land (A \in V \land B \in V)) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ((A \in V \land B \in V) \land χ))$
33	17 19 32	pm5.21nd	$⊢ φ \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land ψ) \leftrightarrow ((A \in V \land B \in V) \land χ))$

Metamath Proof Explorer

Theorem copsex2b

Proof