Theorem vtocl2ga 3537

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2178 and ax-11 2194. (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 343	. . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 → 𝜓) ↔ (𝐴 ∈ 𝐶 → 𝜒)))
3		vtocl2ga.1	. . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	imbi2d 343	. . . . 5 ⊢ (𝑥 = 𝐴 → ((𝑦 ∈ 𝐷 → 𝜑) ↔ (𝑦 ∈ 𝐷 → 𝜓)))
5		vtocl2ga.3	. . . . . 6 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → 𝜑)
6	5	ex 418	. . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑))
7	4, 6	vtoclga 3536	. . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓))
8	7	com12 33	. . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓))
9	2, 8	vtoclga 3536	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒))
10	9	impcom 413	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  vtocl3ga  3540  vtocl4ga  3542  solin  5583  caovcan  7614  xpord2pred  8141  pwfseqlem2  10701  mulcanenq  11002  ltaddnq  11016  ltrnq  11021  genpv  11041  wrdind  14824  fsumrelem  15927  imasleval  17660  fullfunc  18030  fthfunc  18031  symggrplem  19027  pf1ind  22620  mretopd  23357  dvlip  26260  scvxcvx  27262  issubgoilem  31781  cnre2csqlem  34461