Theorem rcla42v 1880

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 1663	. . 3 |- (x = A -> (A.y e. D ph <-> A.y e. D ch))
3	2	rcla4v 1873	. 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 1873	. 2 |- (B e. D -> (A.y e. D ch -> ps))
6	3, 5	sylan9 468	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 956   e. wcel 958  A.wral 1645

This theorem is referenced by:  rcla43v 1882  isorel 3894  isocnv 3896  isotr 3897  isotrALT 3898  foprcl 4015  fiint 4552  seq1rn2 6307  seqzrn2 6542  infxpidmlem7 7543  inopnt 7585  basis1t 7599  basis2t 7600  tgss2t 7622  hausnei 7769  meteq0 7797  metcni 7879  ablcom 8088  ghgrpilem1 8118  nvs 8275  nvtri 8283  phpar2 8467  phpar 8468  logltbt 8761  shaddclt 9070  shaddcltOLD 9071  shmulclt 9072  shmulcltOLD 9073  unopt 9824  hmopt 9831  adjt 9842  hstel2t 10131  stjt 10147  stcltr1 10186  mddmdin0 10343  cdj3lem1 10346  cdj3lem2b 10349  ghomlin 10378  ghomf1olem 10381  filint 10522  cmppfd 10621  domcmpd 10622  codcmpd 10623  cmpida 10650  cmpidb 10651  ismonb2 10681  cmpmon 10684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812

Copyright terms: Public domain