cgsex4gOLD

Description: Obsolete version of cgsex4g as of 21-Mar-2025. (Contributed by NM, 5-Aug-1995) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 28-Jun-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cgsex4gOLD.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to χ$
	cgsex4gOLD.2	$⊢ χ \to (φ \leftrightarrow ψ)$
Assertion	cgsex4gOLD	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w (χ \land φ) \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		cgsex4gOLD.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to χ$
2		cgsex4gOLD.2	$⊢ χ \to (φ \leftrightarrow ψ)$
3	2	biimpa	$⊢ (χ \land φ) \to ψ$
4	3	exlimivv	$⊢ \exists z \exists w (χ \land φ) \to ψ$
5	4	exlimivv	$⊢ \exists x \exists y \exists z \exists w (χ \land φ) \to ψ$
6		elisset	$⊢ A \in R \to \exists x x = A$
7		elisset	$⊢ B \in S \to \exists y y = B$
8	6 7	anim12i	$⊢ (A \in R \land B \in S) \to (\exists x x = A \land \exists y y = B)$
9		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
10	8 9	sylibr	$⊢ (A \in R \land B \in S) \to \exists x \exists y (x = A \land y = B)$
11		elisset	$⊢ C \in R \to \exists z z = C$
12		elisset	$⊢ D \in S \to \exists w w = D$
13	11 12	anim12i	$⊢ (C \in R \land D \in S) \to (\exists z z = C \land \exists w w = D)$
14		exdistrv	$⊢ \exists z \exists w (z = C \land w = D) \leftrightarrow (\exists z z = C \land \exists w w = D)$
15	13 14	sylibr	$⊢ (C \in R \land D \in S) \to \exists z \exists w (z = C \land w = D)$
16	10 15	anim12i	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y (x = A \land y = B) \land \exists z \exists w (z = C \land w = D))$
17		eqeq1	$⊢ y = v \to (y = B \leftrightarrow v = B)$
18	17	anbi2d	$⊢ y = v \to ((x = A \land y = B) \leftrightarrow (x = A \land v = B))$
19	18	anbi1d	$⊢ y = v \to (((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow ((x = A \land v = B) \land (z = C \land w = D)))$
20	19	exbidv	$⊢ y = v \to (\exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \exists w ((x = A \land v = B) \land (z = C \land w = D)))$
21	20	notbid	$⊢ y = v \to (\neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \neg \exists w ((x = A \land v = B) \land (z = C \land w = D)))$
22		eqeq1	$⊢ z = v \to (z = C \leftrightarrow v = C)$
23	22	anbi1d	$⊢ z = v \to ((z = C \land w = D) \leftrightarrow (v = C \land w = D))$
24	23	anbi2d	$⊢ z = v \to (((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow ((x = A \land y = B) \land (v = C \land w = D)))$
25	24	exbidv	$⊢ z = v \to (\exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \exists w ((x = A \land y = B) \land (v = C \land w = D)))$
26	25	notbid	$⊢ z = v \to (\neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \neg \exists w ((x = A \land y = B) \land (v = C \land w = D)))$
27	21 26	alcomw	$⊢ \forall y \forall z \neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \forall z \forall y \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
28	27	notbii	$⊢ \neg \forall y \forall z \neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \neg \forall z \forall y \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
29		2exnaln	$⊢ \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \neg \forall y \forall z \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
30		2exnaln	$⊢ \exists z \exists y \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \neg \forall z \forall y \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
31	28 29 30	3bitr4i	$⊢ \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \exists z \exists y \exists w ((x = A \land y = B) \land (z = C \land w = D))$
32	31	exbii	$⊢ \exists x \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow \exists x \exists z \exists y \exists w ((x = A \land y = B) \land (z = C \land w = D))$
33		4exdistrv	$⊢ \exists x \exists z \exists y \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow (\exists x \exists y (x = A \land y = B) \land \exists z \exists w (z = C \land w = D))$
34	32 33	bitri	$⊢ \exists x \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow (\exists x \exists y (x = A \land y = B) \land \exists z \exists w (z = C \land w = D))$
35	16 34	sylibr	$⊢ ((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))$
36	1	2eximi	$⊢ \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \exists z \exists w χ$
37	36	2eximi	$⊢ \exists x \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \exists x \exists y \exists z \exists w χ$
38	35 37	syl	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to \exists x \exists y \exists z \exists w χ$
39	2	biimprcd	$⊢ ψ \to (χ \to φ)$
40	39	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
41	40	2eximdv	$⊢ ψ \to (\exists z \exists w χ \to \exists z \exists w (χ \land φ))$
42	41	2eximdv	$⊢ ψ \to (\exists x \exists y \exists z \exists w χ \to \exists x \exists y \exists z \exists w (χ \land φ))$
43	38 42	syl5com	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (ψ \to \exists x \exists y \exists z \exists w (χ \land φ))$
44	5 43	impbid2	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to (\exists x \exists y \exists z \exists w (χ \land φ) \leftrightarrow ψ)$

Metamath Proof Explorer

Theorem cgsex4gOLD

Proof