Theorem rspc2v 3596

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 3156	. . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒))
3	2	rspcv 3581	. 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒))
4		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
5	4	rspcv 3581	. 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  3597  rspc3v  3601  rspc6v  3606  disji2  5086  f1veqaeq  7213  isorel  7283  isosolem  7304  oveqrspc2v  7396  fovcld  7496  caovclg  7561  caovcomg  7564  caofidlcan  7671  resf1extb  7890  smoel  8306  fiint  9253  fiintOLD  9254  dffi3  9358  ltordlem  11679  seqhomo  13990  cshf1  14751  climcn2  15535  drsdir  18243  tsrlin  18526  dirge  18544  mgmhmlin  18608  issubmgm2  18612  mhmlin  18702  issubg2  19055  nsgbi  19071  ghmlin  19135  efgi  19633  efgred  19662  rglcom4d  20131  irredmul  20349  issubrng2  20478  issubrg2  20512  abvmul  20741  abvtri  20742  lmodlema  20803  islmodd  20804  rmodislmodlem  20867  rmodislmod  20868  lmhmlin  20974  lbsind  21019  rnglidlmcl  21158  ipcj  21576  obsip  21663  mplcoe5lem  21979  matecl  22345  dmatelnd  22416  scmateALT  22432  mdetdiaglem  22518  mdetdiagid  22520  pmatcoe1fsupp  22621  m2cpminvid2lem  22674  inopn  22819  basis1  22870  basis2  22871  iscldtop  23015  hausnei  23248  t1sep2  23289  nconnsubb  23343  r0sep  23668  fbasssin  23756  fcfneii  23957  ustssel  24126  xmeteq0  24259  tngngp3  24577  nmvs  24597  cncfi  24820  c1lip1  25935  aalioulem3  26275  logltb  26542  cvxcl  26928  2sqlem8  27370  nocvxminlem  27723  madebday  27849  negsproplem1  27974  negsprop  27981  axtgcgrrflx  28442  axtgsegcon  28444  axtg5seg  28445  axtgbtwnid  28446  axtgpasch  28447  axtgcont1  28448  axtgupdim2  28451  axtgeucl  28452  isperp2d  28696  f1otrgds  28849  brbtwn2  28885  axcontlem3  28946  axcontlem9  28952  axcontlem10  28953  upgrwlkdvdelem  29716  conngrv2edg  30174  frgrwopreglem5ALT  30301  ablocom  30527  nvs  30642  nvtri  30649  phpar2  30802  phpar  30803  shaddcl  31196  shmulcl  31197  cnopc  31892  unop  31894  hmop  31901  cnfnc  31909  adj1  31912  hstel2  32198  stj  32214  stcltr1i  32253  mddmdin0i  32410  cdj3lem1  32413  cdj3lem2b  32416  disji2f  32556  disjif2  32560  disjxpin  32567  isoun  32675  archirng  33157  archiexdiv  33159  slmdlema  33172  inelcarsg  34295  sibfof  34324  breprexplema  34614  axtgupdim2ALTV  34652  pconncn  35204  ivthALT  36316  poimirlem32  37639  ismtycnv  37789  ismtyima  37790  ismtyres  37795  bfplem1  37809  bfplem2  37810  ghomlinOLD  37875  rngohomadd  37956  rngohommul  37957  crngocom  37988  idladdcl  38006  idllmulcl  38007  idlrmulcl  38008  pridl  38024  ispridlc  38057  pridlc  38058  dmnnzd  38062  oposlem  39168  omllaw  39229  hlsuprexch  39368  lautle  40071  ltrnu  40108  tendovalco  40752  sticksstones1  42127  sticksstones2  42128  ntrkbimka  44020  relprel  44934  mullimc  45607  mullimcf  45614  lptre2pt  45631  fourierdlem54  46151  fcoresf1  47063  faovcl  47194  icceuelpartlem  47429  iccpartnel  47432  fargshiftf1  47435  sprsymrelfolem2  47487  reuopreuprim  47520  isubgr3stgrlem6  47963  isthincd2lem2  49417