Theorem vtocl2ga 3578

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2141 and ax-11 2157. (Revised by GG, 20-Aug-2023.) (Proof shortened by Wolf Lammen, 23-Aug-2023.)

Hypotheses

Ref	Expression
vtocl2ga.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl2ga.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
vtocl2ga.3	⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)

Assertion

Ref	Expression
vtocl2ga	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥   𝜒,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)   𝐵(𝑥)

Proof of Theorem vtocl2ga

Step	Hyp	Ref	Expression
1		vtocl2ga.2	. . . 4 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
2	1	imbi2d 340	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 → 𝜓) ↔ (𝐴 ∈ 𝐶 → 𝜒)))
3		vtocl2ga.1	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	imbi2d 340	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑦 ∈ 𝐷 → 𝜑) ↔ (𝑦 ∈ 𝐷 → 𝜓)))
5		vtocl2ga.3	. . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)
6	5	ex 412	. . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑))
7	4, 6	vtoclga 3577	. . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓))
8	7	com12 32	. . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓))
9	2, 8	vtoclga 3577	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒))
10	9	impcom 407	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816

This theorem is referenced by:  vtocl3ga  3583  vtocl4ga  3586  solin  5619  caovcan  7637  xpord2pred  8170  pwfseqlem2  10699  mulcanenq  11000  ltaddnq  11014  ltrnq  11019  genpv  11039  wrdind  14760  fsumrelem  15843  imasleval  17586  fullfunc  17953  fthfunc  17954  symggrplem  18897  pf1ind  22359  mretopd  23100  dvlip  26032  scvxcvx  27029  issubgoilem  31279  cnre2csqlem  33909