Theorem rspc2v 3594

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  rspc2va  3595  rspc3v  3599  rspc6v  3604  disji2  5095  f1veqaeq  7259  isorel  7333  isosolem  7354  oveqrspc2v  7446  fovcld  7546  caovclg  7612  caovcomg  7615  caofidlcan  7722  resf1extb  7937  smoel  8353  fiint  9293  dffi3  9398  ltordlem  11756  seqhomo  14105  cshf1  14873  climcn2  15670  drsdir  18382  tsrlin  18665  dirge  18683  mgmhmlin  18791  issubmgm2  18795  mhmlin  18890  issubg2  19254  nsgbi  19269  ghmlin  19337  efgi  19835  efgred  19864  rglcom4d  20339  irredmul  20559  issubrng2  20709  issubrg2  20743  abvmul  20976  abvtri  20977  lmodlema  21038  islmodd  21039  rmodislmodlem  21102  rmodislmod  21103  lmhmlin  21208  lbsind  21253  rnglidlmcl  21393  unichnlidl  21414  ipcj  21836  obsip  21923  mplcoe5lem  22242  matecl  22634  dmatelnd  22705  scmateALT  22721  mdetdiaglem  22807  mdetdiagid  22809  pmatcoe1fsupp  22910  m2cpminvid2lem  22963  inopn  23108  basis1  23159  basis2  23160  iscldtop  23304  hausnei  23537  t1sep2  23578  nconnsubb  23632  r0sep  23958  fbasssin  24046  fcfneii  24247  ustssel  24416  xmeteq0  24548  tngngp3  24866  nmvs  24886  cncfi  25106  c1lip1  26209  aalioulem3  26550  logltb  26818  cvxcl  27202  2sqlem8  27643  nocvxminlem  28000  madebday  28146  negsproplem1  28274  negsprop  28281  axtgcgrrflx  28784  axtgsegcon  28786  axtg5seg  28787  axtgbtwnid  28788  axtgpasch  28789  axtgcont1  28790  axtgupdim2  28793  axtgeucl  28794  isperp2d  29049  f1otrgds  29275  brbtwn2  29312  axcontlem3  29373  axcontlem9  29379  axcontlem10  29380  upgrwlkdvdelem  30151  conngrv2edg  30619  frgrwopreglem5ALT  30746  ablocom  30973  nvs  31088  nvtri  31095  phpar2  31248  phpar  31249  shaddcl  31642  shmulcl  31643  cnopc  32338  unop  32340  hmop  32347  cnfnc  32355  adj1  32358  hstel2  32644  stj  32660  stcltr1i  32699  mddmdin0i  32856  cdj3lem1  32859  cdj3lem2b  32862  disji2f  32995  disjif2  32999  disjxpin  33006  isoun  33120  archirng  33574  archiexdiv  33576  slmdlema  33589  inelcarsg  34768  sibfof  34797  breprexplema  35084  axtgupdim2ALTV  35122  pconncn  35755  ivthALT  36905  poimirlem32  38362  ismtycnv  38513  ismtyima  38514  ismtyres  38519  bfplem1  38533  bfplem2  38534  ghomlinOLD  38599  rngohomadd  38680  rngohommul  38681  crngocom  38712  idladdcl  38730  idllmulcl  38731  idlrmulcl  38732  pridl  38748  ispridlc  38781  pridlc  38782  dmnnzd  38786  oposlem  40016  omllaw  40077  hlsuprexch  40215  lautle  40918  ltrnu  40955  tendovalco  41599  sticksstones1  42973  sticksstones2  42974  ntrkbimka  44824  relprel  45720  mullimc  46392  mullimcf  46399  lptre2pt  46414  fourierdlem54  46934  fcoresf1  47866  faovcl  47997  icceuelpartlem  48244  iccpartnel  48247  fargshiftf1  48250  sprsymrelfolem2  48302  reuopreuprim  48335  isubgr3stgrlem6  48796  idomnzd  49170  isthincd2lem2  50272