Theorem rspc2v 2847

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 1521	. 2 |- F/ x ch
2		nfv 1521	. 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 2845	1 |- ( ( A e. C /\ B e. D ) -> ( A. x e. C A. y e. D ph -> ps ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   A.wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732

This theorem is referenced by:  rspc2va  2848  rspc3v  2850  disji2  3982  ontriexmidim  4506  wetriext  4561  f1veqaeq  5748  isorel  5787  oveqrspc2v  5880  fovcl  5958  caovclg  6005  caovcomg  6008  smoel  6279  dcdifsnid  6483  unfiexmid  6895  fiintim  6906  supmoti  6970  supsnti  6982  isotilem  6983  onntri35  7214  onntri45  7218  cauappcvgprlem1  7621  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprprlemval  7650  ltordlem  8401  frecuzrdgrrn  10364  frec2uzrdg  10365  frecuzrdgrcl  10366  frecuzrdgrclt  10371  seq3caopr3  10437  seq3homo  10466  climcn2  11272  fprodcl2lem  11568  ennnfonelemim  12379  mhmlin  12690  inopn  12795  basis1  12839  basis2  12840  xmeteq0  13153  cncfi  13359  limccnp2lem  13439  logltb  13589  2sqlem8  13753  redcwlpo  14087  redc0  14089  reap0  14090