Theorem rspc2v 3590

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2v	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2v

Step	Hyp	Ref	Expression
1		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2	1	ralbidv 3189	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒))
3	2	rspcv 3576	. 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒))
4		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcv 3576	. 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓))
6	3, 5	sylan9 517	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  rspc2va  3591  rspc3v  3595  rspc6v  3600  disji2  5092  f1veqaeq  7291  isorel  7365  isosolem  7386  oveqrspc2v  7478  fovcld  7578  caovclg  7645  caovcomg  7648  caofidlcan  7763  resf1extb  7980  smoel  8406  fiint  9356  dffi3  9460  ltordlem  11881  seqhomo  14232  cshf1  15003  climcn2  15804  drsdir  18526  tsrlin  18809  dirge  18827  mgmhmlin  18938  issubmgm2  18942  mhmlin  19038  issubg2  19402  nsgbi  19417  ghmlin  19485  efgi  19984  efgred  20013  rglcom4d  20488  irredmul  20710  issubrng2  20861  issubrg2  20895  abvmul  21129  abvtri  21130  lmodlema  21191  islmodd  21192  rmodislmodlem  21255  rmodislmod  21256  lmhmlin  21361  lbsind  21406  rnglidlmcl  21546  unichnlidl  21567  ipcj  21995  obsip  22082  mplcoe5lem  22403  matecl  22795  dmatelnd  22866  scmateALT  22882  mdetdiaglem  22968  mdetdiagid  22970  pmatcoe1fsupp  23074  m2cpminvid2lem  23127  inopn  23272  basis1  23323  basis2  23324  iscldtop  23468  hausnei  23701  t1sep2  23742  nconnsubb  23796  r0sep  24122  fbasssin  24210  fcfneii  24411  ustssel  24580  xmeteq0  24712  tngngp3  25030  nmvs  25050  cncfi  25270  c1lip1  26372  aalioulem3  26718  logltb  26985  cvxcl  27369  2sqlem8  27810  nocvxminlem  28197  madebday  28343  negsproplem1  28471  negsprop  28478  axtgcgrrflx  28981  axtgsegcon  28983  axtg5seg  28984  axtgbtwnid  28985  axtgpasch  28986  axtgcont1  28987  axtgupdim2  28990  axtgeucl  28991  isperp2d  29248  f1otrgds  29503  brbtwn2  29540  axcontlem3  29601  axcontlem9  29607  axcontlem10  29608  upgrwlkdvdelem  30379  conngrv2edg  30853  frgrwopreglem5ALT  30980  ablocom  31207  nvs  31322  nvtri  31329  phpar2  31482  phpar  31483  shaddcl  31876  shmulcl  31877  cnopc  32572  unop  32574  hmop  32581  cnfnc  32589  adj1  32592  hstel2  32878  stj  32894  stcltr1i  32933  mddmdin0i  33090  cdj3lem1  33093  cdj3lem2b  33096  disji2f  33269  disjif2  33273  disjxpin  33280  isoun  33392  archirng  33848  archiexdiv  33850  slmdlema  33863  inelcarsg  35054  sibfof  35083  breprexplema  35370  axtgupdim2ALTV  35408  pconncn  36197  ivthALT  37338  poimirlem32  38838  ismtycnv  39002  ismtyima  39003  ismtyres  39008  bfplem1  39022  bfplem2  39023  ghomlinOLD  39088  rngohomadd  39169  rngohommul  39170  crngocom  39201  idladdcl  39219  idllmulcl  39220  idlrmulcl  39221  pridl  39237  ispridlc  39270  pridlc  39271  dmnnzd  39275  oposlem  40505  omllaw  40566  hlsuprexch  40704  lautle  41407  ltrnu  41444  tendovalco  42088  sticksstones1  43462  sticksstones2  43463  ntrkbimka  45299  relprel  46205  mullimc  46901  mullimcf  46908  lptre2pt  46923  fourierdlem54  47443  fcoresf1  48412  faovcl  48543  icceuelpartlem  48790  iccpartnel  48793  fargshiftf1  48796  sprsymrelfolem2  48848  reuopreuprim  48881  isubgr3stgrlem6  49342  idomnzd  49774  isthincd2lem2  50901