Theorem rspc2v 3587

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  rspc2va  3588  rspc3v  3592  rspc6v  3597  disji2  5087  f1veqaeq  7260  isorel  7334  isosolem  7355  oveqrspc2v  7447  fovcld  7547  caovclg  7613  caovcomg  7616  caofidlcan  7731  resf1extb  7946  smoel  8368  fiint  9318  dffi3  9423  ltordlem  11841  seqhomo  14192  cshf1  14961  climcn2  15760  drsdir  18476  tsrlin  18759  dirge  18777  mgmhmlin  18888  issubmgm2  18892  mhmlin  18988  issubg2  19352  nsgbi  19367  ghmlin  19435  efgi  19933  efgred  19962  rglcom4d  20437  irredmul  20659  issubrng2  20810  issubrg2  20844  abvmul  21078  abvtri  21079  lmodlema  21140  islmodd  21141  rmodislmodlem  21204  rmodislmod  21205  lmhmlin  21310  lbsind  21355  rnglidlmcl  21495  unichnlidl  21516  ipcj  21940  obsip  22027  mplcoe5lem  22348  matecl  22740  dmatelnd  22811  scmateALT  22827  mdetdiaglem  22913  mdetdiagid  22915  pmatcoe1fsupp  23019  m2cpminvid2lem  23072  inopn  23217  basis1  23268  basis2  23269  iscldtop  23413  hausnei  23646  t1sep2  23687  nconnsubb  23741  r0sep  24067  fbasssin  24155  fcfneii  24356  ustssel  24525  xmeteq0  24657  tngngp3  24975  nmvs  24995  cncfi  25215  c1lip1  26317  aalioulem3  26661  logltb  26928  cvxcl  27312  2sqlem8  27753  nocvxminlem  28140  madebday  28286  negsproplem1  28414  negsprop  28421  axtgcgrrflx  28924  axtgsegcon  28926  axtg5seg  28927  axtgbtwnid  28928  axtgpasch  28929  axtgcont1  28930  axtgupdim2  28933  axtgeucl  28934  isperp2d  29191  f1otrgds  29446  brbtwn2  29483  axcontlem3  29544  axcontlem9  29550  axcontlem10  29551  upgrwlkdvdelem  30322  conngrv2edg  30796  frgrwopreglem5ALT  30923  ablocom  31150  nvs  31265  nvtri  31272  phpar2  31425  phpar  31426  shaddcl  31819  shmulcl  31820  cnopc  32515  unop  32517  hmop  32524  cnfnc  32532  adj1  32535  hstel2  32821  stj  32837  stcltr1i  32876  mddmdin0i  33033  cdj3lem1  33036  cdj3lem2b  33039  disji2f  33171  disjif2  33175  disjxpin  33182  isoun  33295  archirng  33749  archiexdiv  33751  slmdlema  33764  inelcarsg  34943  sibfof  34972  breprexplema  35259  axtgupdim2ALTV  35297  pconncn  35989  ivthALT  37123  poimirlem32  38570  ismtycnv  38736  ismtyima  38737  ismtyres  38742  bfplem1  38756  bfplem2  38757  ghomlinOLD  38822  rngohomadd  38903  rngohommul  38904  crngocom  38935  idladdcl  38953  idllmulcl  38954  idlrmulcl  38955  pridl  38971  ispridlc  39004  pridlc  39005  dmnnzd  39009  oposlem  40239  omllaw  40300  hlsuprexch  40438  lautle  41141  ltrnu  41178  tendovalco  41822  sticksstones1  43196  sticksstones2  43197  ntrkbimka  45037  relprel  45940  mullimc  46627  mullimcf  46634  lptre2pt  46649  fourierdlem54  47169  fcoresf1  48138  faovcl  48269  icceuelpartlem  48516  iccpartnel  48519  fargshiftf1  48522  sprsymrelfolem2  48574  reuopreuprim  48607  isubgr3stgrlem6  49068  idomnzd  49442  isthincd2lem2  50542