Theorem rspc2v 3590

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079

This theorem is used by:  rspc2va  3591  rspc3v  3595  rspc6v  3600  disji2  5091  f1veqaeq  7257  isorel  7331  isosolem  7352  oveqrspc2v  7444  fovcld  7544  caovclg  7610  caovcomg  7613  caofidlcan  7720  resf1extb  7935  smoel  8353  fiint  9300  dffi3  9405  ltordlem  11767  seqhomo  14117  cshf1  14885  climcn2  15684  drsdir  18396  tsrlin  18679  dirge  18697  mgmhmlin  18807  issubmgm2  18811  mhmlin  18907  issubg2  19271  nsgbi  19286  ghmlin  19354  efgi  19852  efgred  19881  rglcom4d  20356  irredmul  20576  issubrng2  20726  issubrg2  20760  abvmul  20993  abvtri  20994  lmodlema  21055  islmodd  21056  rmodislmodlem  21119  rmodislmod  21120  lmhmlin  21225  lbsind  21270  rnglidlmcl  21410  unichnlidl  21431  ipcj  21853  obsip  21940  mplcoe5lem  22261  matecl  22653  dmatelnd  22724  scmateALT  22740  mdetdiaglem  22826  mdetdiagid  22828  pmatcoe1fsupp  22932  m2cpminvid2lem  22985  inopn  23130  basis1  23181  basis2  23182  iscldtop  23326  hausnei  23559  t1sep2  23600  nconnsubb  23654  r0sep  23980  fbasssin  24068  fcfneii  24269  ustssel  24438  xmeteq0  24570  tngngp3  24888  nmvs  24908  cncfi  25128  c1lip1  26231  aalioulem3  26577  logltb  26845  cvxcl  27229  2sqlem8  27670  nocvxminlem  28027  madebday  28173  negsproplem1  28301  negsprop  28308  axtgcgrrflx  28811  axtgsegcon  28813  axtg5seg  28814  axtgbtwnid  28815  axtgpasch  28816  axtgcont1  28817  axtgupdim2  28820  axtgeucl  28821  isperp2d  29078  f1otrgds  29333  brbtwn2  29370  axcontlem3  29431  axcontlem9  29437  axcontlem10  29438  upgrwlkdvdelem  30209  conngrv2edg  30683  frgrwopreglem5ALT  30810  ablocom  31037  nvs  31152  nvtri  31159  phpar2  31312  phpar  31313  shaddcl  31706  shmulcl  31707  cnopc  32402  unop  32404  hmop  32411  cnfnc  32419  adj1  32422  hstel2  32708  stj  32724  stcltr1i  32763  mddmdin0i  32920  cdj3lem1  32923  cdj3lem2b  32926  disji2f  33058  disjif2  33062  disjxpin  33069  isoun  33182  archirng  33636  archiexdiv  33638  slmdlema  33651  inelcarsg  34830  sibfof  34859  breprexplema  35146  axtgupdim2ALTV  35184  pconncn  35811  ivthALT  36962  poimirlem32  38409  ismtycnv  38560  ismtyima  38561  ismtyres  38566  bfplem1  38580  bfplem2  38581  ghomlinOLD  38646  rngohomadd  38727  rngohommul  38728  crngocom  38759  idladdcl  38777  idllmulcl  38778  idlrmulcl  38779  pridl  38795  ispridlc  38828  pridlc  38829  dmnnzd  38833  oposlem  40063  omllaw  40124  hlsuprexch  40262  lautle  40965  ltrnu  41002  tendovalco  41646  sticksstones1  43020  sticksstones2  43021  ntrkbimka  44886  relprel  45782  mullimc  46454  mullimcf  46461  lptre2pt  46476  fourierdlem54  46996  fcoresf1  47965  faovcl  48096  icceuelpartlem  48343  iccpartnel  48346  fargshiftf1  48349  sprsymrelfolem2  48401  reuopreuprim  48434  isubgr3stgrlem6  48895  idomnzd  49269  isthincd2lem2  50369