Theorem rspc2v 3585

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

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

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050

This theorem is referenced by:  rspc2va  3586  rspc3v  3590  rspc6v  3595  disji2  5079  f1veqaeq  7199  isorel  7269  isosolem  7290  oveqrspc2v  7382  fovcld  7482  caovclg  7547  caovcomg  7550  caofidlcan  7657  resf1extb  7873  smoel  8289  fiint  9221  dffi3  9325  ltordlem  11652  seqhomo  13966  cshf1  14727  climcn2  15510  drsdir  18218  tsrlin  18501  dirge  18519  mgmhmlin  18617  issubmgm2  18621  mhmlin  18711  issubg2  19064  nsgbi  19079  ghmlin  19143  efgi  19641  efgred  19670  rglcom4d  20139  irredmul  20357  issubrng2  20483  issubrg2  20517  abvmul  20746  abvtri  20747  lmodlema  20808  islmodd  20809  rmodislmodlem  20872  rmodislmod  20873  lmhmlin  20979  lbsind  21024  rnglidlmcl  21163  ipcj  21581  obsip  21668  mplcoe5lem  21984  matecl  22350  dmatelnd  22421  scmateALT  22437  mdetdiaglem  22523  mdetdiagid  22525  pmatcoe1fsupp  22626  m2cpminvid2lem  22679  inopn  22824  basis1  22875  basis2  22876  iscldtop  23020  hausnei  23253  t1sep2  23294  nconnsubb  23348  r0sep  23673  fbasssin  23761  fcfneii  23962  ustssel  24131  xmeteq0  24263  tngngp3  24581  nmvs  24601  cncfi  24824  c1lip1  25939  aalioulem3  26279  logltb  26546  cvxcl  26932  2sqlem8  27374  nocvxminlem  27727  madebday  27855  negsproplem1  27980  negsprop  27987  axtgcgrrflx  28450  axtgsegcon  28452  axtg5seg  28453  axtgbtwnid  28454  axtgpasch  28455  axtgcont1  28456  axtgupdim2  28459  axtgeucl  28460  isperp2d  28704  f1otrgds  28857  brbtwn2  28894  axcontlem3  28955  axcontlem9  28961  axcontlem10  28962  upgrwlkdvdelem  29725  conngrv2edg  30186  frgrwopreglem5ALT  30313  ablocom  30539  nvs  30654  nvtri  30661  phpar2  30814  phpar  30815  shaddcl  31208  shmulcl  31209  cnopc  31904  unop  31906  hmop  31913  cnfnc  31921  adj1  31924  hstel2  32210  stj  32226  stcltr1i  32265  mddmdin0i  32422  cdj3lem1  32425  cdj3lem2b  32428  disji2f  32568  disjif2  32572  disjxpin  32579  isoun  32694  archirng  33168  archiexdiv  33170  slmdlema  33183  inelcarsg  34335  sibfof  34364  breprexplema  34654  axtgupdim2ALTV  34692  pconncn  35279  ivthALT  36390  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  44145  relprel  45058  mullimc  45730  mullimcf  45737  lptre2pt  45752  fourierdlem54  46272  fcoresf1  47183  faovcl  47314  icceuelpartlem  47549  iccpartnel  47552  fargshiftf1  47555  sprsymrelfolem2  47607  reuopreuprim  47640  isubgr3stgrlem6  48085  isthincd2lem2  49550