Theorem rspc2v 3592

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077

This theorem is referenced by:  rspc2va  3593  rspc3v  3597  rspc6v  3602  disji2  5084  f1veqaeq  7240  isorel  7310  isosolem  7331  oveqrspc2v  7423  fovcld  7523  caovclg  7588  caovcomg  7591  caofidlcan  7698  resf1extb  7915  smoel  8331  fiint  9271  dffi3  9377  ltordlem  11712  seqhomo  14062  cshf1  14823  climcn2  15620  drsdir  18334  tsrlin  18617  dirge  18635  mgmhmlin  18733  issubmgm2  18737  mhmlin  18827  issubg2  19183  nsgbi  19198  ghmlin  19261  efgi  19759  efgred  19788  rglcom4d  20261  irredmul  20478  issubrng2  20608  issubrg2  20642  abvmul  20870  abvtri  20871  lmodlema  20932  islmodd  20933  rmodislmodlem  20996  rmodislmod  20997  lmhmlin  21102  lbsind  21147  rnglidlmcl  21286  ipcj  21686  obsip  21773  mplcoe5lem  22092  matecl  22485  dmatelnd  22556  scmateALT  22572  mdetdiaglem  22658  mdetdiagid  22660  pmatcoe1fsupp  22761  m2cpminvid2lem  22814  inopn  22959  basis1  23010  basis2  23011  iscldtop  23155  hausnei  23388  t1sep2  23429  nconnsubb  23483  r0sep  23808  fbasssin  23896  fcfneii  24097  ustssel  24266  xmeteq0  24398  tngngp3  24716  nmvs  24736  cncfi  24956  c1lip1  26059  aalioulem3  26398  logltb  26665  cvxcl  27049  2sqlem8  27490  nocvxminlem  27847  madebday  27993  negsproplem1  28121  negsprop  28128  axtgcgrrflx  28631  axtgsegcon  28633  axtg5seg  28634  axtgbtwnid  28635  axtgpasch  28636  axtgcont1  28637  axtgupdim2  28640  axtgeucl  28641  isperp2d  28889  f1otrgds  29069  brbtwn2  29106  axcontlem3  29167  axcontlem9  29173  axcontlem10  29174  upgrwlkdvdelem  29936  conngrv2edg  30397  frgrwopreglem5ALT  30524  ablocom  30751  nvs  30866  nvtri  30873  phpar2  31026  phpar  31027  shaddcl  31420  shmulcl  31421  cnopc  32116  unop  32118  hmop  32125  cnfnc  32133  adj1  32136  hstel2  32422  stj  32438  stcltr1i  32477  mddmdin0i  32634  cdj3lem1  32637  cdj3lem2b  32640  disji2f  32777  disjif2  32781  disjxpin  32788  isoun  32904  archirng  33368  archiexdiv  33370  slmdlema  33383  inelcarsg  34608  sibfof  34637  breprexplema  34924  axtgupdim2ALTV  34962  pconncn  35574  ivthALT  36695  poimirlem32  38151  ismtycnv  38301  ismtyima  38302  ismtyres  38307  bfplem1  38321  bfplem2  38322  ghomlinOLD  38387  rngohomadd  38468  rngohommul  38469  crngocom  38500  idladdcl  38518  idllmulcl  38519  idlrmulcl  38520  pridl  38536  ispridlc  38569  pridlc  38570  dmnnzd  38574  oposlem  39806  omllaw  39867  hlsuprexch  40005  lautle  40708  ltrnu  40745  tendovalco  41389  sticksstones1  42763  sticksstones2  42764  ntrkbimka  44614  relprel  45527  mullimc  46192  mullimcf  46199  lptre2pt  46214  fourierdlem54  46734  fcoresf1  47663  faovcl  47794  icceuelpartlem  48041  iccpartnel  48044  fargshiftf1  48047  sprsymrelfolem2  48099  reuopreuprim  48132  isubgr3stgrlem6  48593  isthincd2lem2  50056