Theorem rspc2v 2920

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 1574	. 2 |- F/ x ch
2		nfv 1574	. 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 2918	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 1395   e. wcel 2200   A.wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  rspc2va  2921  rspc3v  2923  disji2  4075  ontriexmidim  4614  wetriext  4669  f1veqaeq  5893  isorel  5932  oveqrspc2v  6028  fovcld  6109  caovclg  6158  caovcomg  6161  smoel  6446  dcdifsnid  6650  unfiexmid  7080  prfidceq  7090  fiintim  7093  supmoti  7160  supsnti  7172  isotilem  7173  onntri35  7422  onntri45  7426  cauappcvgprlem1  7846  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprprlemval  7875  ltordlem  8629  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgrclt  10637  seq3caopr3  10713  seq3homo  10749  seqhomog  10752  climcn2  11820  fprodcl2lem  12116  ennnfonelemim  12995  mhmlin  13500  issubg2m  13726  nsgbi  13741  ghmlin  13785  issubrng2  14174  issubrg2  14205  lmodlema  14256  islmodd  14257  rmodislmodlem  14314  rmodislmod  14315  rnglidlmcl  14444  inopn  14677  basis1  14721  basis2  14722  xmeteq0  15033  cncfi  15252  limccnp2lem  15350  logltb  15548  2sqlem8  15802  redcwlpo  16423  redc0  16425  reap0  16426