Theorem rspc2v 3620

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052

This theorem is referenced by:  rspc2va  3621  rspc3v  3625  rspc6v  3629  disji2  5129  f1veqaeq  7263  isorel  7329  isosolem  7350  oveqrspc2v  7442  fovcld  7544  caovclg  7609  caovcomg  7612  smoel  8381  fiint  9360  fiintOLD  9361  dffi3  9466  ltordlem  11779  seqhomo  14062  cshf1  14812  climcn2  15589  drsdir  18321  tsrlin  18604  dirge  18622  mgmhmlin  18686  issubmgm2  18690  mhmlin  18777  issubg2  19130  nsgbi  19146  ghmlin  19210  efgi  19712  efgred  19741  rglcom4d  20189  irredmul  20406  issubrng2  20535  issubrg2  20571  abvmul  20795  abvtri  20796  lmodlema  20836  islmodd  20837  rmodislmodlem  20900  rmodislmod  20901  rmodislmodOLD  20902  lmhmlin  21008  lbsind  21053  rnglidlmcl  21200  ipcj  21625  obsip  21714  mplcoe5lem  22041  matecl  22414  dmatelnd  22485  scmateALT  22501  mdetdiaglem  22587  mdetdiagid  22589  pmatcoe1fsupp  22690  m2cpminvid2lem  22743  inopn  22888  basis1  22940  basis2  22941  iscldtop  23086  hausnei  23319  t1sep2  23360  nconnsubb  23414  r0sep  23739  fbasssin  23827  fcfneii  24028  ustssel  24197  xmeteq0  24331  tngngp3  24660  nmvs  24680  cncfi  24901  c1lip1  26017  aalioulem3  26358  logltb  26623  cvxcl  27009  2sqlem8  27451  nocvxminlem  27803  madebday  27919  negsproplem1  28033  negsprop  28040  axtgcgrrflx  28385  axtgsegcon  28387  axtg5seg  28388  axtgbtwnid  28389  axtgpasch  28390  axtgcont1  28391  axtgupdim2  28394  axtgeucl  28395  isperp2d  28639  f1otrgds  28792  brbtwn2  28835  axcontlem3  28896  axcontlem9  28902  axcontlem10  28903  upgrwlkdvdelem  29669  conngrv2edg  30124  frgrwopreglem5ALT  30251  ablocom  30477  nvs  30592  nvtri  30599  phpar2  30752  phpar  30753  shaddcl  31146  shmulcl  31147  cnopc  31842  unop  31844  hmop  31851  cnfnc  31859  adj1  31862  hstel2  32148  stj  32164  stcltr1i  32203  mddmdin0i  32360  cdj3lem1  32363  cdj3lem2b  32366  disji2f  32496  disjif2  32500  disjxpin  32507  isoun  32612  archirng  33056  archiexdiv  33058  slmdlema  33070  inelcarsg  34157  sibfof  34186  breprexplema  34488  axtgupdim2ALTV  34526  pconncn  35064  ivthALT  36059  poimirlem32  37365  ismtycnv  37515  ismtyima  37516  ismtyres  37521  bfplem1  37535  bfplem2  37536  ghomlinOLD  37601  rngohomadd  37682  rngohommul  37683  crngocom  37714  idladdcl  37732  idllmulcl  37733  idlrmulcl  37734  pridl  37750  ispridlc  37783  pridlc  37784  dmnnzd  37788  oposlem  38892  omllaw  38953  hlsuprexch  39092  lautle  39795  ltrnu  39832  tendovalco  40476  sticksstones1  41857  sticksstones2  41858  ntrkbimka  43741  mullimc  45272  mullimcf  45279  lptre2pt  45296  fourierdlem54  45816  fcoresf1  46719  faovcl  46848  icceuelpartlem  47042  iccpartnel  47045  fargshiftf1  47048  sprsymrelfolem2  47100  reuopreuprim  47133  isthincd2lem2  48392