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  5899  isorel  5938  oveqrspc2v  6034  fovcld  6115  caovclg  6164  caovcomg  6167  smoel  6452  dcdifsnid  6658  unfiexmid  7091  prfidceq  7101  fiintim  7104  supmoti  7171  supsnti  7183  isotilem  7184  onntri35  7433  onntri45  7437  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprprlemval  7886  ltordlem  8640  frecuzrdgrrn  10642  frec2uzrdg  10643  frecuzrdgrcl  10644  frecuzrdgrclt  10649  seq3caopr3  10725  seq3homo  10761  seqhomog  10764  climcn2  11836  fprodcl2lem  12132  ennnfonelemim  13011  mhmlin  13516  issubg2m  13742  nsgbi  13757  ghmlin  13801  issubrng2  14190  issubrg2  14221  lmodlema  14272  islmodd  14273  rmodislmodlem  14330  rmodislmod  14331  rnglidlmcl  14460  inopn  14693  basis1  14737  basis2  14738  xmeteq0  15049  cncfi  15268  limccnp2lem  15366  logltb  15564  2sqlem8  15818  redcwlpo  16511  redc0  16513  reap0  16514