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) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 21-Mar-2025)

	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		elisset	$⊢ C \in R \to \exists z z = C$
10		elisset	$⊢ D \in S \to \exists w w = D$
11	9 10	anim12i	$⊢ (C \in R \land D \in S) \to (\exists z z = C \land \exists w w = D)$
12	8 11	anim12i	$⊢ ((A \in R \land B \in S) \land (C \in R \land D \in S)) \to ((\exists x x = A \land \exists y y = B) \land (\exists z z = C \land \exists w w = D))$
13		19.42vv	$⊢ \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow ((x = A \land y = B) \land \exists z \exists w (z = C \land w = D))$
14	13	2exbii	$⊢ \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))$
15		19.41vv	$⊢ \exists x \exists y ((x = A \land y = B) \land \exists z \exists w (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))$
16		exdistrv	$⊢ \exists x \exists y (x = A \land y = B) \leftrightarrow (\exists x x = A \land \exists y y = B)$
17		exdistrv	$⊢ \exists z \exists w (z = C \land w = D) \leftrightarrow (\exists z z = C \land \exists w w = D)$
18	16 17	anbi12i	$⊢ (\exists x \exists y (x = A \land y = B) \land \exists z \exists w (z = C \land w = D)) \leftrightarrow ((\exists x x = A \land \exists y y = B) \land (\exists z z = C \land \exists w w = D))$
19	14 15 18	3bitri	$⊢ \exists x \exists y \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \leftrightarrow ((\exists x x = A \land \exists y y = B) \land (\exists z z = C \land \exists w w = D))$
20	12 19	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))$
21	1	2eximi	$⊢ \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \exists z \exists w χ$
22	21	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 χ$
23	20 22	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 χ$
24	2	biimprcd	$⊢ ψ \to (χ \to φ)$
25	24	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
26	25	2eximdv	$⊢ ψ \to (\exists z \exists w χ \to \exists z \exists w (χ \land φ))$
27	26	2eximdv	$⊢ ψ \to (\exists x \exists y \exists z \exists w χ \to \exists x \exists y \exists z \exists w (χ \land φ))$
28	23 27	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 φ))$
29	5 28	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