Theorem rspc2v 3575

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspc2va  3576  rspc3v  3580  rspc6v  3585  disji2  5069  f1veqaeq  7211  isorel  7281  isosolem  7302  oveqrspc2v  7394  fovcld  7494  caovclg  7559  caovcomg  7562  caofidlcan  7669  resf1extb  7885  smoel  8300  fiint  9237  dffi3  9344  ltordlem  11675  seqhomo  14011  cshf1  14772  climcn2  15555  drsdir  18268  tsrlin  18551  dirge  18569  mgmhmlin  18667  issubmgm2  18671  mhmlin  18761  issubg2  19117  nsgbi  19132  ghmlin  19196  efgi  19694  efgred  19723  rglcom4d  20192  irredmul  20409  issubrng2  20535  issubrg2  20569  abvmul  20798  abvtri  20799  lmodlema  20860  islmodd  20861  rmodislmodlem  20924  rmodislmod  20925  lmhmlin  21030  lbsind  21075  rnglidlmcl  21214  ipcj  21614  obsip  21701  mplcoe5lem  22017  matecl  22390  dmatelnd  22461  scmateALT  22477  mdetdiaglem  22563  mdetdiagid  22565  pmatcoe1fsupp  22666  m2cpminvid2lem  22719  inopn  22864  basis1  22915  basis2  22916  iscldtop  23060  hausnei  23293  t1sep2  23334  nconnsubb  23388  r0sep  23713  fbasssin  23801  fcfneii  24002  ustssel  24171  xmeteq0  24303  tngngp3  24621  nmvs  24641  cncfi  24861  c1lip1  25964  aalioulem3  26300  logltb  26564  cvxcl  26948  2sqlem8  27389  nocvxminlem  27746  madebday  27892  negsproplem1  28020  negsprop  28027  axtgcgrrflx  28530  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  axtgupdim2  28539  axtgeucl  28540  isperp2d  28784  f1otrgds  28937  brbtwn2  28974  axcontlem3  29035  axcontlem9  29041  axcontlem10  29042  upgrwlkdvdelem  29804  conngrv2edg  30265  frgrwopreglem5ALT  30392  ablocom  30619  nvs  30734  nvtri  30741  phpar2  30894  phpar  30895  shaddcl  31288  shmulcl  31289  cnopc  31984  unop  31986  hmop  31993  cnfnc  32001  adj1  32004  hstel2  32290  stj  32306  stcltr1i  32345  mddmdin0i  32502  cdj3lem1  32505  cdj3lem2b  32508  disji2f  32647  disjif2  32651  disjxpin  32658  isoun  32775  archirng  33249  archiexdiv  33251  slmdlema  33264  inelcarsg  34455  sibfof  34484  breprexplema  34774  axtgupdim2ALTV  34812  pconncn  35406  ivthALT  36517  poimirlem32  37973  ismtycnv  38123  ismtyima  38124  ismtyres  38129  bfplem1  38143  bfplem2  38144  ghomlinOLD  38209  rngohomadd  38290  rngohommul  38291  crngocom  38322  idladdcl  38340  idllmulcl  38341  idlrmulcl  38342  pridl  38358  ispridlc  38391  pridlc  38392  dmnnzd  38396  oposlem  39628  omllaw  39689  hlsuprexch  39827  lautle  40530  ltrnu  40567  tendovalco  41211  sticksstones1  42585  sticksstones2  42586  ntrkbimka  44465  relprel  45378  mullimc  46046  mullimcf  46053  lptre2pt  46068  fourierdlem54  46588  fcoresf1  47517  faovcl  47648  icceuelpartlem  47895  iccpartnel  47898  fargshiftf1  47901  sprsymrelfolem2  47953  reuopreuprim  47986  isubgr3stgrlem6  48447  isthincd2lem2  49910