Theorem vtocl2ga 3532

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.) Avoid ax-10 2147 and ax-11 2163. (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 3531	. . . 4 ⊢ (𝐴 ∈ 𝐶 → (𝑦 ∈ 𝐷 → 𝜓))
8	7	com12 32	. . 3 ⊢ (𝑦 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜓))
9	2, 8	vtoclga 3531	. 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → 𝜒))
10	9	impcom 407	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 𝜒)

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810

This theorem is referenced by:  vtocl3ga  3537  vtocl4ga  3540  solin  5558  caovcan  7562  xpord2pred  8087  pwfseqlem2  10572  mulcanenq  10873  ltaddnq  10887  ltrnq  10892  genpv  10912  wrdind  14647  fsumrelem  15732  imasleval  17464  fullfunc  17834  fthfunc  17835  symggrplem  18811  pf1ind  22301  mretopd  23038  dvlip  25956  scvxcvx  26954  issubgoilem  31316  cnre2csqlem  34046