Theorem rspc2v 3583

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

This theorem is referenced by:  rspc2va  3584  rspc3v  3588  rspc6v  3593  disji2  5073  f1veqaeq  7190  isorel  7260  isosolem  7281  oveqrspc2v  7373  fovcld  7473  caovclg  7538  caovcomg  7541  caofidlcan  7648  resf1extb  7864  smoel  8280  fiint  9211  dffi3  9315  ltordlem  11642  seqhomo  13956  cshf1  14717  climcn2  15500  drsdir  18208  tsrlin  18491  dirge  18509  mgmhmlin  18607  issubmgm2  18611  mhmlin  18701  issubg2  19054  nsgbi  19069  ghmlin  19133  efgi  19631  efgred  19660  rglcom4d  20129  irredmul  20347  issubrng2  20473  issubrg2  20507  abvmul  20736  abvtri  20737  lmodlema  20798  islmodd  20799  rmodislmodlem  20862  rmodislmod  20863  lmhmlin  20969  lbsind  21014  rnglidlmcl  21153  ipcj  21571  obsip  21658  mplcoe5lem  21974  matecl  22340  dmatelnd  22411  scmateALT  22427  mdetdiaglem  22513  mdetdiagid  22515  pmatcoe1fsupp  22616  m2cpminvid2lem  22669  inopn  22814  basis1  22865  basis2  22866  iscldtop  23010  hausnei  23243  t1sep2  23284  nconnsubb  23338  r0sep  23663  fbasssin  23751  fcfneii  23952  ustssel  24121  xmeteq0  24253  tngngp3  24571  nmvs  24591  cncfi  24814  c1lip1  25929  aalioulem3  26269  logltb  26536  cvxcl  26922  2sqlem8  27364  nocvxminlem  27717  madebday  27845  negsproplem1  27970  negsprop  27977  axtgcgrrflx  28440  axtgsegcon  28442  axtg5seg  28443  axtgbtwnid  28444  axtgpasch  28445  axtgcont1  28446  axtgupdim2  28449  axtgeucl  28450  isperp2d  28694  f1otrgds  28847  brbtwn2  28883  axcontlem3  28944  axcontlem9  28950  axcontlem10  28951  upgrwlkdvdelem  29714  conngrv2edg  30175  frgrwopreglem5ALT  30302  ablocom  30528  nvs  30643  nvtri  30650  phpar2  30803  phpar  30804  shaddcl  31197  shmulcl  31198  cnopc  31893  unop  31895  hmop  31902  cnfnc  31910  adj1  31913  hstel2  32199  stj  32215  stcltr1i  32254  mddmdin0i  32411  cdj3lem1  32414  cdj3lem2b  32417  disji2f  32557  disjif2  32561  disjxpin  32568  isoun  32683  archirng  33157  archiexdiv  33159  slmdlema  33172  inelcarsg  34324  sibfof  34353  breprexplema  34643  axtgupdim2ALTV  34681  pconncn  35268  ivthALT  36379  poimirlem32  37702  ismtycnv  37852  ismtyima  37853  ismtyres  37858  bfplem1  37872  bfplem2  37873  ghomlinOLD  37938  rngohomadd  38019  rngohommul  38020  crngocom  38051  idladdcl  38069  idllmulcl  38070  idlrmulcl  38071  pridl  38087  ispridlc  38120  pridlc  38121  dmnnzd  38125  oposlem  39291  omllaw  39352  hlsuprexch  39490  lautle  40193  ltrnu  40230  tendovalco  40874  sticksstones1  42249  sticksstones2  42250  ntrkbimka  44141  relprel  45054  mullimc  45726  mullimcf  45733  lptre2pt  45748  fourierdlem54  46268  fcoresf1  47179  faovcl  47310  icceuelpartlem  47545  iccpartnel  47548  fargshiftf1  47551  sprsymrelfolem2  47603  reuopreuprim  47636  isubgr3stgrlem6  48081  isthincd2lem2  49546