Theorem rspc2v 3571

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  rspc2va  3572  rspc3v  3576  rspc6v  3581  disji2  5056  f1veqaeq  7200  isorel  7270  isosolem  7291  oveqrspc2v  7383  fovcld  7483  caovclg  7548  caovcomg  7551  caofidlcan  7658  resf1extb  7874  smoel  8290  fiint  9227  dffi3  9334  ltordlem  11666  seqhomo  14002  cshf1  14763  climcn2  15546  drsdir  18259  tsrlin  18542  dirge  18560  mgmhmlin  18658  issubmgm2  18662  mhmlin  18752  issubg2  19108  nsgbi  19123  ghmlin  19187  efgi  19685  efgred  19714  rglcom4d  20183  irredmul  20400  issubrng2  20530  issubrg2  20564  abvmul  20793  abvtri  20794  lmodlema  20855  islmodd  20856  rmodislmodlem  20919  rmodislmod  20920  lmhmlin  21025  lbsind  21070  rnglidlmcl  21209  ipcj  21609  obsip  21696  mplcoe5lem  22015  matecl  22408  dmatelnd  22479  scmateALT  22495  mdetdiaglem  22581  mdetdiagid  22583  pmatcoe1fsupp  22684  m2cpminvid2lem  22737  inopn  22882  basis1  22933  basis2  22934  iscldtop  23078  hausnei  23311  t1sep2  23352  nconnsubb  23406  r0sep  23731  fbasssin  23819  fcfneii  24020  ustssel  24189  xmeteq0  24321  tngngp3  24639  nmvs  24659  cncfi  24879  c1lip1  25982  aalioulem3  26318  logltb  26582  cvxcl  26966  2sqlem8  27407  nocvxminlem  27764  madebday  27910  negsproplem1  28038  negsprop  28045  axtgcgrrflx  28548  axtgsegcon  28550  axtg5seg  28551  axtgbtwnid  28552  axtgpasch  28553  axtgcont1  28554  axtgupdim2  28557  axtgeucl  28558  isperp2d  28802  f1otrgds  28955  brbtwn2  28992  axcontlem3  29053  axcontlem9  29059  axcontlem10  29060  upgrwlkdvdelem  29822  conngrv2edg  30283  frgrwopreglem5ALT  30410  ablocom  30637  nvs  30752  nvtri  30759  phpar2  30912  phpar  30913  shaddcl  31306  shmulcl  31307  cnopc  32002  unop  32004  hmop  32011  cnfnc  32019  adj1  32022  hstel2  32308  stj  32324  stcltr1i  32363  mddmdin0i  32520  cdj3lem1  32523  cdj3lem2b  32526  disji2f  32666  disjif2  32670  disjxpin  32677  isoun  32794  archirng  33269  archiexdiv  33271  slmdlema  33284  inelcarsg  34495  sibfof  34524  breprexplema  34814  axtgupdim2ALTV  34852  pconncn  35452  ivthALT  36563  poimirlem32  38019  ismtycnv  38169  ismtyima  38170  ismtyres  38175  bfplem1  38189  bfplem2  38190  ghomlinOLD  38255  rngohomadd  38336  rngohommul  38337  crngocom  38368  idladdcl  38386  idllmulcl  38387  idlrmulcl  38388  pridl  38404  ispridlc  38437  pridlc  38438  dmnnzd  38442  oposlem  39674  omllaw  39735  hlsuprexch  39873  lautle  40576  ltrnu  40613  tendovalco  41257  sticksstones1  42631  sticksstones2  42632  ntrkbimka  44482  relprel  45395  mullimc  46061  mullimcf  46068  lptre2pt  46083  fourierdlem54  46603  fcoresf1  47532  faovcl  47663  icceuelpartlem  47910  iccpartnel  47913  fargshiftf1  47916  sprsymrelfolem2  47968  reuopreuprim  48001  isubgr3stgrlem6  48462  isthincd2lem2  49925