Theorem rspc2v 3585

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 3157	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒))
3	2	rspcv 3570	. 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒))
4		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcv 3570	. 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓))
6	3, 5	sylan9 507	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050

This theorem is referenced by:  rspc2va  3586  rspc3v  3590  rspc6v  3595  disji2  5080  f1veqaeq  7200  isorel  7270  isosolem  7291  oveqrspc2v  7383  fovcld  7483  caovclg  7548  caovcomg  7551  caofidlcan  7658  resf1extb  7874  smoel  8290  fiint  9225  dffi3  9332  ltordlem  11660  seqhomo  13970  cshf1  14731  climcn2  15514  drsdir  18223  tsrlin  18506  dirge  18524  mgmhmlin  18622  issubmgm2  18626  mhmlin  18716  issubg2  19069  nsgbi  19084  ghmlin  19148  efgi  19646  efgred  19675  rglcom4d  20144  irredmul  20363  issubrng2  20489  issubrg2  20523  abvmul  20752  abvtri  20753  lmodlema  20814  islmodd  20815  rmodislmodlem  20878  rmodislmod  20879  lmhmlin  20985  lbsind  21030  rnglidlmcl  21169  ipcj  21587  obsip  21674  mplcoe5lem  21992  matecl  22367  dmatelnd  22438  scmateALT  22454  mdetdiaglem  22540  mdetdiagid  22542  pmatcoe1fsupp  22643  m2cpminvid2lem  22696  inopn  22841  basis1  22892  basis2  22893  iscldtop  23037  hausnei  23270  t1sep2  23311  nconnsubb  23365  r0sep  23690  fbasssin  23778  fcfneii  23979  ustssel  24148  xmeteq0  24280  tngngp3  24598  nmvs  24618  cncfi  24841  c1lip1  25956  aalioulem3  26296  logltb  26563  cvxcl  26949  2sqlem8  27391  nocvxminlem  27744  madebday  27872  negsproplem1  27997  negsprop  28004  axtgcgrrflx  28483  axtgsegcon  28485  axtg5seg  28486  axtgbtwnid  28487  axtgpasch  28488  axtgcont1  28489  axtgupdim2  28492  axtgeucl  28493  isperp2d  28737  f1otrgds  28890  brbtwn2  28927  axcontlem3  28988  axcontlem9  28994  axcontlem10  28995  upgrwlkdvdelem  29758  conngrv2edg  30219  frgrwopreglem5ALT  30346  ablocom  30572  nvs  30687  nvtri  30694  phpar2  30847  phpar  30848  shaddcl  31241  shmulcl  31242  cnopc  31937  unop  31939  hmop  31946  cnfnc  31954  adj1  31957  hstel2  32243  stj  32259  stcltr1i  32298  mddmdin0i  32455  cdj3lem1  32458  cdj3lem2b  32461  disji2f  32601  disjif2  32605  disjxpin  32612  isoun  32730  archirng  33219  archiexdiv  33221  slmdlema  33234  inelcarsg  34417  sibfof  34446  breprexplema  34736  axtgupdim2ALTV  34774  pconncn  35367  ivthALT  36478  poimirlem32  37792  ismtycnv  37942  ismtyima  37943  ismtyres  37948  bfplem1  37962  bfplem2  37963  ghomlinOLD  38028  rngohomadd  38109  rngohommul  38110  crngocom  38141  idladdcl  38159  idllmulcl  38160  idlrmulcl  38161  pridl  38177  ispridlc  38210  pridlc  38211  dmnnzd  38215  oposlem  39381  omllaw  39442  hlsuprexch  39580  lautle  40283  ltrnu  40320  tendovalco  40964  sticksstones1  42339  sticksstones2  42340  ntrkbimka  44221  relprel  45134  mullimc  45804  mullimcf  45811  lptre2pt  45826  fourierdlem54  46346  fcoresf1  47257  faovcl  47388  icceuelpartlem  47623  iccpartnel  47626  fargshiftf1  47629  sprsymrelfolem2  47681  reuopreuprim  47714  isubgr3stgrlem6  48159  isthincd2lem2  49622