vtocl4ga

Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019)

	Ref	Expression
Hypotheses	vtocl4ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	vtocl4ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
	vtocl4ga.3	$⊢ z = C \to (χ \leftrightarrow ρ)$
	vtocl4ga.4	$⊢ w = D \to (ρ \leftrightarrow θ)$
	vtocl4ga.5	$⊢ ((x \in Q \land y \in R) \land (z \in S \land w \in T)) \to φ$
Assertion	vtocl4ga	$⊢ ((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ$

Proof

Step	Hyp	Ref	Expression
1		vtocl4ga.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		vtocl4ga.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		vtocl4ga.3	$⊢ z = C \to (χ \leftrightarrow ρ)$
4		vtocl4ga.4	$⊢ w = D \to (ρ \leftrightarrow θ)$
5		vtocl4ga.5	$⊢ ((x \in Q \land y \in R) \land (z \in S \land w \in T)) \to φ$
6		eleq1	$⊢ x = A \to (x \in Q \leftrightarrow A \in Q)$
7	6	anbi1d	$⊢ x = A \to ((x \in Q \land y \in R) \leftrightarrow (A \in Q \land y \in R))$
8	7	anbi1d	$⊢ x = A \to (((x \in Q \land y \in R) \land (z \in S \land w \in T)) \leftrightarrow ((A \in Q \land y \in R) \land (z \in S \land w \in T)))$
9	8 1	imbi12d	$⊢ x = A \to ((((x \in Q \land y \in R) \land (z \in S \land w \in T)) \to φ) \leftrightarrow (((A \in Q \land y \in R) \land (z \in S \land w \in T)) \to ψ))$
10		eleq1	$⊢ y = B \to (y \in R \leftrightarrow B \in R)$
11	10	anbi2d	$⊢ y = B \to ((A \in Q \land y \in R) \leftrightarrow (A \in Q \land B \in R))$
12	11	anbi1d	$⊢ y = B \to (((A \in Q \land y \in R) \land (z \in S \land w \in T)) \leftrightarrow ((A \in Q \land B \in R) \land (z \in S \land w \in T)))$
13	12 2	imbi12d	$⊢ y = B \to ((((A \in Q \land y \in R) \land (z \in S \land w \in T)) \to ψ) \leftrightarrow (((A \in Q \land B \in R) \land (z \in S \land w \in T)) \to χ))$
14		eleq1	$⊢ z = C \to (z \in S \leftrightarrow C \in S)$
15	14	anbi1d	$⊢ z = C \to ((z \in S \land w \in T) \leftrightarrow (C \in S \land w \in T))$
16	15	anbi2d	$⊢ z = C \to (((A \in Q \land B \in R) \land (z \in S \land w \in T)) \leftrightarrow ((A \in Q \land B \in R) \land (C \in S \land w \in T)))$
17	16 3	imbi12d	$⊢ z = C \to ((((A \in Q \land B \in R) \land (z \in S \land w \in T)) \to χ) \leftrightarrow (((A \in Q \land B \in R) \land (C \in S \land w \in T)) \to ρ))$
18		eleq1	$⊢ w = D \to (w \in T \leftrightarrow D \in T)$
19	18	anbi2d	$⊢ w = D \to ((C \in S \land w \in T) \leftrightarrow (C \in S \land D \in T))$
20	19	anbi2d	$⊢ w = D \to (((A \in Q \land B \in R) \land (C \in S \land w \in T)) \leftrightarrow ((A \in Q \land B \in R) \land (C \in S \land D \in T)))$
21	20 4	imbi12d	$⊢ w = D \to ((((A \in Q \land B \in R) \land (C \in S \land w \in T)) \to ρ) \leftrightarrow (((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ))$
22	9 13 17 21 5	vtocl4g	$⊢ ((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to (((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ)$
23	22	pm2.43i	$⊢ ((A \in Q \land B \in R) \land (C \in S \land D \in T)) \to θ$

Metamath Proof Explorer

Theorem vtocl4ga

Proof