Metamath Proof Explorer

Theorem copsex4g

Description: An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995)

		Ref	Expression
	Hypothesis	copsex4g.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to (φ \leftrightarrow ψ)$
	Assertion	copsex4g	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w ((⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \land φ) \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		copsex4g.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to (φ \leftrightarrow ψ)$
2		eqcom	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = ⟨A, B⟩$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	opth	$⊢ ⟨x, y⟩ = ⟨A, B⟩ \leftrightarrow (x = A \land y = B)$
6	2 5	bitri	$⊢ ⟨A, B⟩ = ⟨x, y⟩ \leftrightarrow (x = A \land y = B)$
7		eqcom	$⊢ ⟨C, D⟩ = ⟨z, w⟩ \leftrightarrow ⟨z, w⟩ = ⟨C, D⟩$
8		vex	$⊢ z \in V$
9		vex	$⊢ w \in V$
10	8 9	opth	$⊢ ⟨z, w⟩ = ⟨C, D⟩ \leftrightarrow (z = C \land w = D)$
11	7 10	bitri	$⊢ ⟨C, D⟩ = ⟨z, w⟩ \leftrightarrow (z = C \land w = D)$
12	6 11	anbi12i	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \leftrightarrow ((x = A \land y = B) \land (z = C \land w = D))$
13	12	anbi1i	$⊢ ((⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \land φ) \leftrightarrow (((x = A \land y = B) \land (z = C \land w = D)) \land φ)$
14	13	a1i	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (((⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \land φ) \leftrightarrow (((x = A \land y = B) \land (z = C \land w = D)) \land φ))$
15	14	4exbidv	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w ((⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \land φ) \leftrightarrow \exists x \exists y \exists z \exists w (((x = A \land y = B) \land (z = C \land w = D)) \land φ))$
16		id	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to ((x = A \land y = B) \land (z = C \land w = D))$
17	16 1	cgsex4g	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w (((x = A \land y = B) \land (z = C \land w = D)) \land φ) \leftrightarrow ψ)$
18	15 17	bitrd	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w ((⟨A, B⟩ = ⟨x, y⟩ \land ⟨C, D⟩ = ⟨z, w⟩) \land φ) \leftrightarrow ψ)$