Theorem rspc2v 3602

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rspc2va  3603  rspc3v  3607  rspc6v  3612  disji2  5094  f1veqaeq  7234  isorel  7304  isosolem  7325  oveqrspc2v  7417  fovcld  7519  caovclg  7584  caovcomg  7587  caofidlcan  7694  resf1extb  7913  smoel  8332  fiint  9284  fiintOLD  9285  dffi3  9389  ltordlem  11710  seqhomo  14021  cshf1  14782  climcn2  15566  drsdir  18270  tsrlin  18551  dirge  18569  mgmhmlin  18633  issubmgm2  18637  mhmlin  18727  issubg2  19080  nsgbi  19096  ghmlin  19160  efgi  19656  efgred  19685  rglcom4d  20127  irredmul  20345  issubrng2  20474  issubrg2  20508  abvmul  20737  abvtri  20738  lmodlema  20778  islmodd  20779  rmodislmodlem  20842  rmodislmod  20843  lmhmlin  20949  lbsind  20994  rnglidlmcl  21133  ipcj  21550  obsip  21637  mplcoe5lem  21953  matecl  22319  dmatelnd  22390  scmateALT  22406  mdetdiaglem  22492  mdetdiagid  22494  pmatcoe1fsupp  22595  m2cpminvid2lem  22648  inopn  22793  basis1  22844  basis2  22845  iscldtop  22989  hausnei  23222  t1sep2  23263  nconnsubb  23317  r0sep  23642  fbasssin  23730  fcfneii  23931  ustssel  24100  xmeteq0  24233  tngngp3  24551  nmvs  24571  cncfi  24794  c1lip1  25909  aalioulem3  26249  logltb  26516  cvxcl  26902  2sqlem8  27344  nocvxminlem  27696  madebday  27818  negsproplem1  27941  negsprop  27948  axtgcgrrflx  28396  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgcont1  28402  axtgupdim2  28405  axtgeucl  28406  isperp2d  28650  f1otrgds  28803  brbtwn2  28839  axcontlem3  28900  axcontlem9  28906  axcontlem10  28907  upgrwlkdvdelem  29673  conngrv2edg  30131  frgrwopreglem5ALT  30258  ablocom  30484  nvs  30599  nvtri  30606  phpar2  30759  phpar  30760  shaddcl  31153  shmulcl  31154  cnopc  31849  unop  31851  hmop  31858  cnfnc  31866  adj1  31869  hstel2  32155  stj  32171  stcltr1i  32210  mddmdin0i  32367  cdj3lem1  32370  cdj3lem2b  32373  disji2f  32513  disjif2  32517  disjxpin  32524  isoun  32632  archirng  33149  archiexdiv  33151  slmdlema  33163  inelcarsg  34309  sibfof  34338  breprexplema  34628  axtgupdim2ALTV  34666  pconncn  35218  ivthALT  36330  poimirlem32  37653  ismtycnv  37803  ismtyima  37804  ismtyres  37809  bfplem1  37823  bfplem2  37824  ghomlinOLD  37889  rngohomadd  37970  rngohommul  37971  crngocom  38002  idladdcl  38020  idllmulcl  38021  idlrmulcl  38022  pridl  38038  ispridlc  38071  pridlc  38072  dmnnzd  38076  oposlem  39182  omllaw  39243  hlsuprexch  39382  lautle  40085  ltrnu  40122  tendovalco  40766  sticksstones1  42141  sticksstones2  42142  ntrkbimka  44034  relprel  44948  mullimc  45621  mullimcf  45628  lptre2pt  45645  fourierdlem54  46165  fcoresf1  47074  faovcl  47205  icceuelpartlem  47440  iccpartnel  47443  fargshiftf1  47446  sprsymrelfolem2  47498  reuopreuprim  47531  isubgr3stgrlem6  47974  isthincd2lem2  49428