cgsex4g

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

	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		excom	$⊢ \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))$
18	17	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))$
19		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))$
20	18 19	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))$
21	16 20	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))$
22	1	2eximi	$⊢ \exists z \exists w ((x = A \land y = B) \land (z = C \land w = D)) \to \exists z \exists w χ$
23	22	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 χ$
24	21 23	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 χ$
25	2	biimprcd	$⊢ ψ \to (χ \to φ)$
26	25	ancld	$⊢ ψ \to (χ \to (χ \land φ))$
27	26	2eximdv	$⊢ ψ \to (\exists z \exists w χ \to \exists z \exists w (χ \land φ))$
28	27	2eximdv	$⊢ ψ \to (\exists x \exists y \exists z \exists w χ \to \exists x \exists y \exists z \exists w (χ \land φ))$
29	24 28	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 φ))$
30	5 29	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