Theorem vtocl2g 3463

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995.)

Hypotheses

Ref	Expression
vtocl2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
vtocl2g.2	⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
vtocl2g.3	⊢ 𝜑

Assertion

Ref	Expression
vtocl2g	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

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

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

Proof of Theorem vtocl2g

Step	Hyp	Ref	Expression
1		nfcv 2948	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2948	. 2 ⊢ Ⅎ𝑦𝐴
3		nfcv 2948	. 2 ⊢ Ⅎ𝑦𝐵
4		nfv 2005	. 2 ⊢ Ⅎ𝑥𝜓
5		nfv 2005	. 2 ⊢ Ⅎ𝑦𝜒
6		vtocl2g.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7		vtocl2g.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
8		vtocl2g.3	. 2 ⊢ 𝜑
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gf 3461	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393

This theorem is referenced by:  vtocl4g  3470  uniprg  4644  intprg  4703  opthg  5135  opelopabsb  5180  vtoclr  5364  elimasng  5701  cnvsngOLD  5835  funopg  6131  f1osng  6389  fsng  6623  fvsng  6668  fnpr2g  6695  unexb  7184  op1stg  7406  op2ndg  7407  xpsneng  8280  xpcomeng  8287  sbth  8315  unxpdom  8402  fpwwe2lem5  9737  prcdnq  10096  mhmlem  17736  carsgmon  30700  br1steqgOLD  31992  br2ndeqgOLD  31993  brimageg  32353  brdomaing  32361  brrangeg  32362  rankung  32592  mbfresfi  33766  zindbi  38009  2sbc6g  39112  2sbc5g  39113  fmulcl  40290