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  32645  archirng  33131  archiexdiv  33133  slmdlema  33146  inelcarsg  34285  sibfof  34314  breprexplema  34604  axtgupdim2ALTV  34642  pconncn  35207  ivthALT  36319  poimirlem32  37642  ismtycnv  37792  ismtyima  37793  ismtyres  37798  bfplem1  37812  bfplem2  37813  ghomlinOLD  37878  rngohomadd  37959  rngohommul  37960  crngocom  37991  idladdcl  38009  idllmulcl  38010  idlrmulcl  38011  pridl  38027  ispridlc  38060  pridlc  38061  dmnnzd  38065  oposlem  39171  omllaw  39232  hlsuprexch  39370  lautle  40073  ltrnu  40110  tendovalco  40754  sticksstones1  42129  sticksstones2  42130  ntrkbimka  44021  relprel  44935  mullimc  45607  mullimcf  45614  lptre2pt  45631  fourierdlem54  46151  fcoresf1  47063  faovcl  47194  icceuelpartlem  47429  iccpartnel  47432  fargshiftf1  47435  sprsymrelfolem2  47487  reuopreuprim  47520  isubgr3stgrlem6  47965  isthincd2lem2  49430