cgsex4g

Description: An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 28-Jun-2024)

	Ref	Expression
Hypotheses	cgsex4g.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to χ$
	cgsex4g.2	$⊢ χ \to (φ \leftrightarrow ψ)$
Assertion	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 (χ \land φ) \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		cgsex4g.1	$⊢ ((x = A \land y = B) \land (z = C \land w = D)) \to χ$
2		cgsex4g.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	$⊢ z = v \to (z = C \leftrightarrow v = C)$
18	17	anbi1d	$⊢ z = v \to ((z = C \land w = D) \leftrightarrow (v = C \land w = D))$
19	18	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)))$
20	19	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)))$
21	20	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)))$
22	21	alcomiw	$⊢ \forall y \forall z \neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \forall z \forall y \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
23		eqeq1	$⊢ y = v \to (y = B \leftrightarrow v = B)$
24	23	anbi2d	$⊢ y = v \to ((x = A \land y = B) \leftrightarrow (x = A \land v = B))$
25	24	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)))$
26	25	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)))$
27	26	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)))$
28	27	alcomiw	$⊢ \forall z \forall y \neg \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \forall y \forall z \neg \exists w ((x = A \land y = B) \land (z = C \land w = D))$
29	22 28	impbii	$⊢ \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))$
30	29	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))$
31		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))$
32		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))$
33	30 31 32	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))$
34	33	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))$
35		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))$
36	34 35	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))$
37	16 36	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))$
38	1	2eximi	$⊢ \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \exists z \exists w χ$
39	38	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 χ$
40	37 39	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 χ$
41	2	biimprcd	$⊢ ψ \to (χ \to φ)$
42	41	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
43	42	2eximdv	$⊢ ψ \to (\exists z \exists w χ \to \exists z \exists w (χ \land φ))$
44	43	2eximdv	$⊢ ψ \to (\exists x \exists y \exists z \exists w χ \to \exists x \exists y \exists z \exists w (χ \land φ))$
45	40 44	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 φ))$
46	5 45	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 cgsex4g

Proof