Theorem rspc2v 3579

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062

This theorem is referenced by:  rspc2va  3580  rspc3v  3582  disji2  5074  f1veqaeq  7186  isorel  7253  isosolem  7274  oveqrspc2v  7364  fovcl  7464  caovclg  7526  caovcomg  7529  smoel  8261  fiint  9189  dffi3  9288  ltordlem  11601  seqhomo  13871  cshf1  14621  climcn2  15401  drsdir  18117  tsrlin  18400  dirge  18418  mhmlin  18534  issubg2  18866  nsgbi  18881  ghmlin  18935  efgi  19420  efgred  19449  irredmul  20046  issubrg2  20149  abvmul  20195  abvtri  20196  lmodlema  20234  islmodd  20235  rmodislmodlem  20296  rmodislmod  20297  rmodislmodOLD  20298  lmhmlin  20403  lbsind  20448  ipcj  20945  obsip  21034  mplcoe5lem  21346  matecl  21680  dmatelnd  21751  scmateALT  21767  mdetdiaglem  21853  mdetdiagid  21855  pmatcoe1fsupp  21956  m2cpminvid2lem  22009  inopn  22154  basis1  22206  basis2  22207  iscldtop  22352  hausnei  22585  t1sep2  22626  nconnsubb  22680  r0sep  23005  fbasssin  23093  fcfneii  23294  ustssel  23463  xmeteq0  23597  tngngp3  23926  nmvs  23946  cncfi  24163  c1lip1  25267  aalioulem3  25600  logltb  25861  cvxcl  26240  2sqlem8  26680  nocvxminlem  27023  axtgcgrrflx  27112  axtgsegcon  27114  axtg5seg  27115  axtgbtwnid  27116  axtgpasch  27117  axtgcont1  27118  axtgupdim2  27121  axtgeucl  27122  isperp2d  27366  f1otrgds  27519  brbtwn2  27562  axcontlem3  27623  axcontlem9  27629  axcontlem10  27630  upgrwlkdvdelem  28392  conngrv2edg  28847  frgrwopreglem5ALT  28974  ablocom  29198  nvs  29313  nvtri  29320  phpar2  29473  phpar  29474  shaddcl  29867  shmulcl  29868  cnopc  30563  unop  30565  hmop  30572  cnfnc  30580  adj1  30583  hstel2  30869  stj  30885  stcltr1i  30924  mddmdin0i  31081  cdj3lem1  31084  cdj3lem2b  31087  disji2f  31203  disjif2  31207  disjxpin  31214  fovcld  31262  isoun  31321  archirng  31729  archiexdiv  31731  slmdlema  31743  inelcarsg  32578  sibfof  32607  breprexplema  32910  axtgupdim2ALTV  32948  pconncn  33485  madebday  34176  ivthALT  34620  poimirlem32  35922  ismtycnv  36073  ismtyima  36074  ismtyres  36079  bfplem1  36093  bfplem2  36094  ghomlinOLD  36159  rngohomadd  36240  rngohommul  36241  crngocom  36272  idladdcl  36290  idllmulcl  36291  idlrmulcl  36292  pridl  36308  ispridlc  36341  pridlc  36342  dmnnzd  36346  oposlem  37457  omllaw  37518  hlsuprexch  37657  lautle  38360  ltrnu  38397  tendovalco  39041  sticksstones1  40367  sticksstones2  40368  ntrkbimka  41978  mullimc  43502  mullimcf  43509  lptre2pt  43526  fourierdlem54  44046  fcoresf1  44923  faovcl  45052  icceuelpartlem  45247  iccpartnel  45250  fargshiftf1  45253  sprsymrelfolem2  45305  reuopreuprim  45338  mgmhmlin  45700  issubmgm2  45704  isthincd2lem2  46677