Theorem vtocl2ga 3566

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2137 and ax-11 2154. (Revised by Gino Giotto, 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 413	. . . . 5 ⊢ (𝑥 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜑))
7	4, 6	vtoclga 3565	. . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓))
8	7	com12 32	. . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓))
9	2, 8	vtoclga 3565	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒))
10	9	impcom 408	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810

This theorem is referenced by:  solin  5613  caovcan  7613  xpord2pred  8133  pwfseqlem2  10656  mulcanenq  10957  ltaddnq  10971  ltrnq  10976  genpv  10996  wrdind  14674  fsumrelem  15755  imasleval  17489  fullfunc  17859  fthfunc  17860  symggrplem  18767  pf1ind  21881  mretopd  22603  dvlip  25517  scvxcvx  26497  issubgoilem  30551  cnre2csqlem  32959