opbrop

Description: Ordered pair membership in a relation. Special case. (Contributed by NM, 5-Aug-1995)

	Ref	Expression
Hypotheses	opbrop.1	$⊢ ((z = A \land w = B) \land (v = C \land u = D)) \to (φ \leftrightarrow ψ)$
	opbrop.2	$⊢ R = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ))\}$
Assertion	opbrop	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		opbrop.1	$⊢ ((z = A \land w = B) \land (v = C \land u = D)) \to (φ \leftrightarrow ψ)$
2		opbrop.2	$⊢ R = \{⟨x, y⟩ \| ((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ))\}$
3		opelxpi	$⊢ (A \in S \land B \in S) \to ⟨A, B⟩ \in (S \times S)$
4		opelxpi	$⊢ (C \in S \land D \in S) \to ⟨C, D⟩ \in (S \times S)$
5	3 4	anim12i	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S))$
6		opex	$⊢ ⟨A, B⟩ \in V$
7		opex	$⊢ ⟨C, D⟩ \in V$
8		eleq1	$⊢ x = ⟨A, B⟩ \to (x \in (S \times S) \leftrightarrow ⟨A, B⟩ \in (S \times S))$
9	8	anbi1d	$⊢ x = ⟨A, B⟩ \to ((x \in (S \times S) \land y \in (S \times S)) \leftrightarrow (⟨A, B⟩ \in (S \times S) \land y \in (S \times S)))$
10		eqeq1	$⊢ x = ⟨A, B⟩ \to (x = ⟨z, w⟩ \leftrightarrow ⟨A, B⟩ = ⟨z, w⟩)$
11	10	anbi1d	$⊢ x = ⟨A, B⟩ \to ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \leftrightarrow (⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩))$
12	11	anbi1d	$⊢ x = ⟨A, B⟩ \to (((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ) \leftrightarrow ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ))$
13	12	4exbidv	$⊢ x = ⟨A, B⟩ \to (\exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ) \leftrightarrow \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ))$
14	9 13	anbi12d	$⊢ x = ⟨A, B⟩ \to (((x \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ)) \leftrightarrow ((⟨A, B⟩ \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ)))$
15		eleq1	$⊢ y = ⟨C, D⟩ \to (y \in (S \times S) \leftrightarrow ⟨C, D⟩ \in (S \times S))$
16	15	anbi2d	$⊢ y = ⟨C, D⟩ \to ((⟨A, B⟩ \in (S \times S) \land y \in (S \times S)) \leftrightarrow (⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)))$
17		eqeq1	$⊢ y = ⟨C, D⟩ \to (y = ⟨v, u⟩ \leftrightarrow ⟨C, D⟩ = ⟨v, u⟩)$
18	17	anbi2d	$⊢ y = ⟨C, D⟩ \to ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \leftrightarrow (⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩))$
19	18	anbi1d	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ) \leftrightarrow ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ))$
20	19	4exbidv	$⊢ y = ⟨C, D⟩ \to (\exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ) \leftrightarrow \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ))$
21	16 20	anbi12d	$⊢ y = ⟨C, D⟩ \to (((⟨A, B⟩ \in (S \times S) \land y \in (S \times S)) \land \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land y = ⟨v, u⟩) \land φ)) \leftrightarrow ((⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)) \land \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ)))$
22	6 7 14 21 2	brab	$⊢ ⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow ((⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)) \land \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ))$
23	1	copsex4g	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (\exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ) \leftrightarrow ψ)$
24	23	anbi2d	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (((⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)) \land \exists z \exists w \exists v \exists u ((⟨A, B⟩ = ⟨z, w⟩ \land ⟨C, D⟩ = ⟨v, u⟩) \land φ)) \leftrightarrow ((⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)) \land ψ))$
25	22 24	syl5bb	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow ((⟨A, B⟩ \in (S \times S) \land ⟨C, D⟩ \in (S \times S)) \land ψ))$
26	5 25	mpbirand	$⊢ ((A \in S \land B \in S) \land (C \in S \land D \in S)) \to (⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem opbrop

Proof