Theorem rspc2v 2923

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 1576	. 2 |- F/ x ch
2		nfv 1576	. 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 2921	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 1397   e. wcel 2202   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspc2va  2924  rspc3v  2926  disji2  4080  ontriexmidim  4620  wetriext  4675  f1veqaeq  5913  isorel  5952  oveqrspc2v  6048  fovcld  6129  caovclg  6178  caovcomg  6181  smoel  6469  dcdifsnid  6675  unfiexmid  7113  prfidceq  7123  fiintim  7126  supmoti  7195  supsnti  7207  isotilem  7208  onntri35  7458  onntri45  7462  cauappcvgprlem1  7882  caucvgprlemnkj  7889  caucvgprlemnbj  7890  caucvgprprlemval  7911  ltordlem  8665  frecuzrdgrrn  10674  frec2uzrdg  10675  frecuzrdgrcl  10676  frecuzrdgrclt  10681  seq3caopr3  10757  seq3homo  10793  seqhomog  10796  climcn2  11890  fprodcl2lem  12187  ennnfonelemim  13066  mhmlin  13571  issubg2m  13797  nsgbi  13812  ghmlin  13856  issubrng2  14246  issubrg2  14277  lmodlema  14328  islmodd  14329  rmodislmodlem  14386  rmodislmod  14387  rnglidlmcl  14516  inopn  14754  basis1  14798  basis2  14799  xmeteq0  15110  cncfi  15329  limccnp2lem  15427  logltb  15625  2sqlem8  15879  redcwlpo  16719  redc0  16721  reap0  16722