Theorem vtocl2g 1841

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 968	. 2 |- (ps -> A.xps)
2		ax-17 968	. 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 1840	1 |- ((A e. C /\ B e. D) -> ch)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955

This theorem is referenced by:  prssg 2463  uniprg 2506  opthgg 2779  unexb 2864  vtoclr 3201  opelcog 3279  elimasng 3411  funopg 3533  funbrfv 3735  op2ndg 4072  ensymg 4392  xpsneng 4416  xpcomeng 4420  xpdom1g 4424  sbth 4437  en2lp 4574  unidomg 4781  unxpdom 4816  prcdpq 5069  fillsb 10435

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain