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  5910  isorel  5949  oveqrspc2v  6045  fovcld  6126  caovclg  6175  caovcomg  6178  smoel  6466  dcdifsnid  6672  unfiexmid  7110  prfidceq  7120  fiintim  7123  supmoti  7192  supsnti  7204  isotilem  7205  onntri35  7455  onntri45  7459  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprprlemval  7908  ltordlem  8662  frecuzrdgrrn  10670  frec2uzrdg  10671  frecuzrdgrcl  10672  frecuzrdgrclt  10677  seq3caopr3  10753  seq3homo  10789  seqhomog  10792  climcn2  11870  fprodcl2lem  12167  ennnfonelemim  13046  mhmlin  13551  issubg2m  13777  nsgbi  13792  ghmlin  13836  issubrng2  14226  issubrg2  14257  lmodlema  14308  islmodd  14309  rmodislmodlem  14366  rmodislmod  14367  rnglidlmcl  14496  inopn  14729  basis1  14773  basis2  14774  xmeteq0  15085  cncfi  15304  limccnp2lem  15402  logltb  15600  2sqlem8  15854  redcwlpo  16662  redc0  16664  reap0  16665