Theorem vtocl2g 3421

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 2913	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2913	. 2 ⊢ Ⅎ𝑦𝐴
3		nfcv 2913	. 2 ⊢ Ⅎ𝑦𝐵
4		nfv 1995	. 2 ⊢ Ⅎ𝑥𝜓
5		nfv 1995	. 2 ⊢ Ⅎ𝑦𝜒
6		vtocl2g.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7		vtocl2g.2	. 2 ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒))
8		vtocl2g.3	. 2 ⊢ 𝜑
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gf 3419	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝜒)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353

This theorem is referenced by:  vtocl4g  3428  ifexg  4296  uniprg  4588  intprg  4645  opthg  5073  opelopabsb  5118  vtoclr  5304  elimasng  5632  cnvsngOLD  5765  funopg  6065  f1osng  6318  fsng  6547  fvsng  6591  fnpr2g  6618  unexb  7105  op1stg  7327  op2ndg  7328  xpsneng  8201  xpcomeng  8208  sbth  8236  unxpdom  8323  fpwwe2lem5  9658  prcdnq  10017  mhmlem  17743  carsgmon  30716  br1steqgOLD  32010  br2ndeqgOLD  32011  brimageg  32371  brdomaing  32379  brrangeg  32380  rankung  32610  mbfresfi  33788  zindbi  38037  2sbc6g  39142  2sbc5g  39143  fmulcl  40331