Theorem rspc2v 2936

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)

Hypotheses

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

Assertion

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

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

Allowed substitution hints:   ph( x, y)   ps( x)   ch( y)   B( x)   C( y)

Proof of Theorem rspc2v

Step	Hyp	Ref	Expression
1		nfv 1577	. 2 |- F/ x ch
2		nfv 1577	. 2 |- F/ y ps
3		rspc2v.1	. 2 |- ( x = A -> ( ph <-> ch ) )
4		rspc2v.2	. 2 |- ( y = B -> ( ch <-> ps ) )
5	1, 2, 3, 4	rspc2 2934	1 |- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph -> ps ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2205   A.wral 2522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817

This theorem is referenced by:  rspc2va  2937  rspc3v  2939  disji2  4103  ontriexmidim  4646  wetriext  4701  f1veqaeq  5944  isorel  5983  oveqrspc2v  6079  fovcld  6160  caovclg  6209  caovcomg  6212  smoel  6533  dcdifsnid  6739  unfiexmid  7180  prfidceq  7190  fiintim  7193  supmoti  7286  supsnti  7298  isotilem  7299  onntri35  7549  onntri45  7553  cauappcvgprlem1  7976  caucvgprlemnkj  7983  caucvgprlemnbj  7984  caucvgprprlemval  8005  ltordlem  8758  frecuzrdgrrn  10774  frec2uzrdg  10775  frecuzrdgrcl  10776  frecuzrdgrclt  10781  seq3caopr3  10857  seq3homo  10893  seqhomog  10896  climcn2  11998  fprodcl2lem  12295  ennnfonelemim  13192  mhmlin  13697  issubg2m  13923  nsgbi  13938  ghmlin  13982  issubrng2  14372  issubrg2  14403  lmodlema  14457  islmodd  14458  rmodislmodlem  14515  rmodislmod  14516  rnglidlmcl  14645  inopn  14885  basis1  14929  basis2  14930  xmeteq0  15241  cncfi  15460  limccnp2lem  15558  logltb  15756  2sqlem8  16013  redcwlpo  16857  redc0  16859  reap0  16860