This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem copsex2g

Description: Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995) Use a similar proof to copsex4g to reduce axiom usage. (Revised by SN, 1-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		copsex2g.1	$⊢ (x = A \land y = B) \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	6	anbi1i	$⊢ (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ((x = A \land y = B) \land φ)$
8	7	2exbii	$⊢ \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y ((x = A \land y = B) \land φ)$
9		id	$⊢ (x = A \land y = B) \to (x = A \land y = B)$
10	9 1	cgsex2g	$⊢ (A \in V \land B \in W) \to (\exists x \exists y ((x = A \land y = B) \land φ) \leftrightarrow ψ)$
11	8 10	bitrid	$⊢ (A \in V \land B \in W) \to (\exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land φ) \leftrightarrow ψ)$