Theorem vtocl2g 2919

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

Hypotheses

Ref	Expression
vtocl2g.1	⊢ (x = A → (φ ↔ ψ))
vtocl2g.2	⊢ (y = B → (ψ ↔ χ))
vtocl2g.3	⊢ φ

Assertion

Ref	Expression
vtocl2g	⊢ ((A ∈ V ∧ B ∈ W) → χ)

Distinct variable groups:   x,A   y,A   y,B   ψ,x   χ,y

Allowed substitution hints:   φ(x,y)   ψ(y)   χ(x)   B(x)   V(x,y)   W(x,y)

Proof of Theorem vtocl2g

Step	Hyp	Ref	Expression
1		nfcv 2490	. 2 ⊢ ℲxA
2		nfcv 2490	. 2 ⊢ ℲyA
3		nfcv 2490	. 2 ⊢ ℲyB
4		nfv 1619	. 2 ⊢ Ⅎxψ
5		nfv 1619	. 2 ⊢ Ⅎyχ
6		vtocl2g.1	. 2 ⊢ (x = A → (φ ↔ ψ))
7		vtocl2g.2	. 2 ⊢ (y = B → (ψ ↔ χ))
8		vtocl2g.3	. 2 ⊢ φ
9	1, 2, 3, 4, 5, 6, 7, 8	vtocl2gf 2917	1 ⊢ ((A ∈ V ∧ B ∈ W) → χ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862

This theorem is referenced by:  ifexg  3722  uniprg  3907  intprg  3961  ninexg  4098  preqr2g  4127  preaddccan2lem1  4455  spfinsfincl  4540  opelopabsb  4698  br1stg  4731  vtoclr  4817  fnunsn  5191  f1osng  5324  fsng  5434  fvsng  5447  trtxp  5782  oqelins4  5795  qrpprod  5837  clos1exg  5878  clos1conn  5880  clos1basesucg  5885  mapex  6007  xpsneng  6051  xpcomeng  6054  enpw1  6063  enmap2  6069  enpw  6088  addccan2nclem2  6265