Theorem vtocl2g 2918

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 2489	. 2 ⊢ ℲxA
2		nfcv 2489	. 2 ⊢ ℲyA
3		nfcv 2489	. 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 2916	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 2478  df-v 2861

This theorem is referenced by:  ifexg  3721  uniprg  3906  intprg  3960  ninexg  4097  preqr2g  4126  preaddccan2lem1  4454  spfinsfincl  4539  opelopabsb  4697  br1stg  4730  vtoclr  4816  fnunsn  5190  f1osng  5323  fsng  5433  fvsng  5446  trtxp  5781  oqelins4  5794  qrpprod  5836  clos1exg  5877  clos1conn  5879  clos1basesucg  5884  mapex  6006  xpsneng  6050  xpcomeng  6053  enpw1  6062  enmap2  6068  enpw  6087  addccan2nclem2  6264