Theorem rspc2v 2897

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 1552	. 2 |- F/ x ch
2		nfv 1552	. 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 2895	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 1373   e. wcel 2178   A.wral 2486

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778

This theorem is referenced by:  rspc2va  2898  rspc3v  2900  disji2  4051  ontriexmidim  4588  wetriext  4643  f1veqaeq  5861  isorel  5900  oveqrspc2v  5994  fovcld  6073  caovclg  6122  caovcomg  6125  smoel  6409  dcdifsnid  6613  unfiexmid  7041  prfidceq  7051  fiintim  7054  supmoti  7121  supsnti  7133  isotilem  7134  onntri35  7383  onntri45  7387  cauappcvgprlem1  7807  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprprlemval  7836  ltordlem  8590  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgrclt  10597  seq3caopr3  10673  seq3homo  10709  seqhomog  10712  climcn2  11735  fprodcl2lem  12031  ennnfonelemim  12910  mhmlin  13414  issubg2m  13640  nsgbi  13655  ghmlin  13699  issubrng2  14087  issubrg2  14118  lmodlema  14169  islmodd  14170  rmodislmodlem  14227  rmodislmod  14228  rnglidlmcl  14357  inopn  14590  basis1  14634  basis2  14635  xmeteq0  14946  cncfi  15165  limccnp2lem  15263  logltb  15461  2sqlem8  15715  redcwlpo  16196  redc0  16198  reap0  16199