Theorem rspc2v 3588

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2va  3589  rspc3v  3593  rspc6v  3598  disji2  5076  f1veqaeq  7193  isorel  7263  isosolem  7284  oveqrspc2v  7376  fovcld  7476  caovclg  7541  caovcomg  7544  caofidlcan  7651  resf1extb  7867  smoel  8283  fiint  9216  fiintOLD  9217  dffi3  9321  ltordlem  11645  seqhomo  13956  cshf1  14716  climcn2  15500  drsdir  18208  tsrlin  18491  dirge  18509  mgmhmlin  18573  issubmgm2  18577  mhmlin  18667  issubg2  19020  nsgbi  19036  ghmlin  19100  efgi  19598  efgred  19627  rglcom4d  20096  irredmul  20314  issubrng2  20443  issubrg2  20477  abvmul  20706  abvtri  20707  lmodlema  20768  islmodd  20769  rmodislmodlem  20832  rmodislmod  20833  lmhmlin  20939  lbsind  20984  rnglidlmcl  21123  ipcj  21541  obsip  21628  mplcoe5lem  21944  matecl  22310  dmatelnd  22381  scmateALT  22397  mdetdiaglem  22483  mdetdiagid  22485  pmatcoe1fsupp  22586  m2cpminvid2lem  22639  inopn  22784  basis1  22835  basis2  22836  iscldtop  22980  hausnei  23213  t1sep2  23254  nconnsubb  23308  r0sep  23633  fbasssin  23721  fcfneii  23922  ustssel  24091  xmeteq0  24224  tngngp3  24542  nmvs  24562  cncfi  24785  c1lip1  25900  aalioulem3  26240  logltb  26507  cvxcl  26893  2sqlem8  27335  nocvxminlem  27688  madebday  27814  negsproplem1  27939  negsprop  27946  axtgcgrrflx  28407  axtgsegcon  28409  axtg5seg  28410  axtgbtwnid  28411  axtgpasch  28412  axtgcont1  28413  axtgupdim2  28416  axtgeucl  28417  isperp2d  28661  f1otrgds  28814  brbtwn2  28850  axcontlem3  28911  axcontlem9  28917  axcontlem10  28918  upgrwlkdvdelem  29681  conngrv2edg  30139  frgrwopreglem5ALT  30266  ablocom  30492  nvs  30607  nvtri  30614  phpar2  30767  phpar  30768  shaddcl  31161  shmulcl  31162  cnopc  31857  unop  31859  hmop  31866  cnfnc  31874  adj1  31877  hstel2  32163  stj  32179  stcltr1i  32218  mddmdin0i  32375  cdj3lem1  32378  cdj3lem2b  32381  disji2f  32521  disjif2  32525  disjxpin  32532  isoun  32644  archirng  33130  archiexdiv  33132  slmdlema  33145  inelcarsg  34279  sibfof  34308  breprexplema  34598  axtgupdim2ALTV  34636  pconncn  35201  ivthALT  36313  poimirlem32  37636  ismtycnv  37786  ismtyima  37787  ismtyres  37792  bfplem1  37806  bfplem2  37807  ghomlinOLD  37872  rngohomadd  37953  rngohommul  37954  crngocom  37985  idladdcl  38003  idllmulcl  38004  idlrmulcl  38005  pridl  38021  ispridlc  38054  pridlc  38055  dmnnzd  38059  oposlem  39165  omllaw  39226  hlsuprexch  39364  lautle  40067  ltrnu  40104  tendovalco  40748  sticksstones1  42123  sticksstones2  42124  ntrkbimka  44015  relprel  44929  mullimc  45601  mullimcf  45608  lptre2pt  45625  fourierdlem54  46145  fcoresf1  47057  faovcl  47188  icceuelpartlem  47423  iccpartnel  47426  fargshiftf1  47429  sprsymrelfolem2  47481  reuopreuprim  47514  isubgr3stgrlem6  47959  isthincd2lem2  49424