Theorem rcla42v 1883

Description: 2-variable restricted specialization with implicit substitution.

Hypotheses

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

Assertion

Ref	Expression
rcla42v	|- ((A e. C /\ B e. D) -> (A.x e. C A.y e. D ph -> ps))

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

Proof of Theorem rcla42v

Step	Hyp	Ref	Expression
1		rcla42v.1	. . . 4 |- (x = A -> (ph <-> ch))
2	1	ralbidv 1666	. . 3 |- (x = A -> (A.y e. D ph <-> A.y e. D ch))
3	2	rcla4v 1876	. 2 |- (A e. C -> (A.x e. C A.y e. D ph -> A.y e. D ch))
4		rcla42v.2	. . 3 |- (y = B -> (ch <-> ps))
5	4	rcla4v 1876	. 2 |- (B e. D -> (A.y e. D ch -> ps))
6	3, 5	sylan9 470	1 |- ((A e. C /\ B e. D) -> (A.x e. C A.y e. D ph -> ps))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  A.wral 1648

This theorem is referenced by:  rcla43v 1885  isorel 3900  isocnv 3902  isotr 3903  isotrALT 3904  foprcl 4021  fiint 4572  fiintOLD 4573  seq1rn2 6322  seqzrn2 6557  infxpidmlem7 7559  inopnt 7601  basis1t 7613  basis2t 7614  tgss2t 7636  hausnei 7781  meteq0 7809  metcni 7891  ablcom 8099  ghgrpilem1 8129  nvs 8286  nvtri 8294  phpar2 8478  phpar 8479  logltbt 8771  shaddclt 9080  shaddcltOLD 9081  shmulclt 9082  shmulcltOLD 9083  unopt 9834  hmopt 9841  adjt 9852  hstel2t 10141  stjt 10157  stcltr1 10196  mddmdin0 10353  cdj3lem1 10356  cdj3lem2b 10359  ghomlin 10388  ghomf1olem 10391  filint 10548  cmppfd 10649  domcmpd 10650  codcmpd 10651  cmpida 10678  cmpidb 10679  ismonb2 10711  cmpmon 10714  isepib2 10721

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815

Copyright terms: Public domain