This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vtocl2gaf

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 10-Aug-2013) (Proof shortened by Wolf Lammen, 31-May-2025)

		Ref	Expression
	Hypotheses	vtocl2gaf.a	⊢ Ⅎ 𝑥 𝐴
		vtocl2gaf.b	⊢ Ⅎ 𝑦 𝐴
		vtocl2gaf.c	⊢ Ⅎ 𝑦 𝐵
		vtocl2gaf.1	⊢ Ⅎ 𝑥 𝜓
		vtocl2gaf.2	⊢ Ⅎ 𝑦 𝜒
		vtocl2gaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
		vtocl2gaf.4	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
		vtocl2gaf.5	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
	Assertion	vtocl2gaf	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		vtocl2gaf.a	⊢ Ⅎ 𝑥 𝐴
2		vtocl2gaf.b	⊢ Ⅎ 𝑦 𝐴
3		vtocl2gaf.c	⊢ Ⅎ 𝑦 𝐵
4		vtocl2gaf.1	⊢ Ⅎ 𝑥 𝜓
5		vtocl2gaf.2	⊢ Ⅎ 𝑦 𝜒
6		vtocl2gaf.3	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
7		vtocl2gaf.4	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
8		vtocl2gaf.5	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
9	2	nfel1	⊢ Ⅎ 𝑦 𝐴 ∈ 𝐶
10	9 5	nfim	⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝐶 → 𝜒 )
11	7	imbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 → 𝜓 ) ↔ ( 𝐴 ∈ 𝐶 → 𝜒 ) ) )
12		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷
13	12 4	nfim	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐷 → 𝜓 )
14	6	imbi2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ∈ 𝐷 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐷 → 𝜓 ) ) )
15	8	ex	⊢ ( 𝑥 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜑 ) )
16	1 13 14 15	vtoclgaf	⊢ ( 𝐴 ∈ 𝐶 → ( 𝑦 ∈ 𝐷 → 𝜓 ) )
17	16	com12	⊢ ( 𝑦 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜓 ) )
18	3 10 11 17	vtoclgaf	⊢ ( 𝐵 ∈ 𝐷 → ( 𝐴 ∈ 𝐶 → 𝜒 ) )
19	18	impcom	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )