Theorem vtocl2g 2349

Description: Implicit substitution of 2 classes for 2 set variables.

Hypotheses

Ref	Expression
vtocl2g.1	|- (x = A -> (ph <-> ps))
vtocl2g.2	|- (y = B -> (ps <-> ch))
vtocl2g.3	|- ph

Assertion

Ref	Expression
vtocl2g	|- ((A e. C /\ B e. D) -> ch)

Distinct variable groups:   x,A   y,A   y,B   ps,x   ch,y

Proof of Theorem vtocl2g

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ps -> A.xps)
2		ax-17 1317	. 2 |- (ch -> A.ych)
3		vtocl2g.1	. 2 |- (x = A -> (ph <-> ps))
4		vtocl2g.2	. 2 |- (y = B -> (ps <-> ch))
5		vtocl2g.3	. 2 |- ph
6	1, 2, 3, 4, 5	vtocl2gf 2348	1 |- ((A e. C /\ B e. D) -> ch)

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300

This theorem is referenced by:  prssgOLD 3141  uniprg 3192  intprg 3251  opthgg 3534  unexb 3797  vtoclr 4032  opelco2g 4133  elimasng 4291  funopg 4454  funsng 4465  funbrfv 4709  op2ndg 5029  ensymg 5470  xpsneng 5495  xpcomeng 5499  xpdom1g 5503  sbth 5520  xpfi 5632  en2lp 5707  unidomg 5971  unxpdom 5996  cdaung 6071  cdaeng 6074  prcdpq 6249  txbas 8933  fillsb 10270  predbrg 13897  surjsec2 14467  iscst2 14520  subtr 15352  subtr2 15353  xpeng 15691  fvopabf4g 15703  seq11g 15804  seq1p1g 15805  seqz1g 15806  seqzp1g 15807  seq1seqzg 15808  2sbc6g 16379  2sbc5g 16380

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain