Theorem rspc2v 3589

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspc2va  3590  rspc3v  3594  rspc6v  3599  disji2  5084  f1veqaeq  7212  isorel  7282  isosolem  7303  oveqrspc2v  7395  fovcld  7495  caovclg  7560  caovcomg  7563  caofidlcan  7670  resf1extb  7886  smoel  8302  fiint  9239  dffi3  9346  ltordlem  11674  seqhomo  13984  cshf1  14745  climcn2  15528  drsdir  18237  tsrlin  18520  dirge  18538  mgmhmlin  18636  issubmgm2  18640  mhmlin  18730  issubg2  19083  nsgbi  19098  ghmlin  19162  efgi  19660  efgred  19689  rglcom4d  20158  irredmul  20377  issubrng2  20503  issubrg2  20537  abvmul  20766  abvtri  20767  lmodlema  20828  islmodd  20829  rmodislmodlem  20892  rmodislmod  20893  lmhmlin  20999  lbsind  21044  rnglidlmcl  21183  ipcj  21601  obsip  21688  mplcoe5lem  22006  matecl  22381  dmatelnd  22452  scmateALT  22468  mdetdiaglem  22554  mdetdiagid  22556  pmatcoe1fsupp  22657  m2cpminvid2lem  22710  inopn  22855  basis1  22906  basis2  22907  iscldtop  23051  hausnei  23284  t1sep2  23325  nconnsubb  23379  r0sep  23704  fbasssin  23792  fcfneii  23993  ustssel  24162  xmeteq0  24294  tngngp3  24612  nmvs  24632  cncfi  24855  c1lip1  25970  aalioulem3  26310  logltb  26577  cvxcl  26963  2sqlem8  27405  nocvxminlem  27762  madebday  27908  negsproplem1  28036  negsprop  28043  axtgcgrrflx  28546  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  axtgupdim2  28555  axtgeucl  28556  isperp2d  28800  f1otrgds  28953  brbtwn2  28990  axcontlem3  29051  axcontlem9  29057  axcontlem10  29058  upgrwlkdvdelem  29821  conngrv2edg  30282  frgrwopreglem5ALT  30409  ablocom  30636  nvs  30751  nvtri  30758  phpar2  30911  phpar  30912  shaddcl  31305  shmulcl  31306  cnopc  32001  unop  32003  hmop  32010  cnfnc  32018  adj1  32021  hstel2  32307  stj  32323  stcltr1i  32362  mddmdin0i  32519  cdj3lem1  32522  cdj3lem2b  32525  disji2f  32664  disjif2  32668  disjxpin  32675  isoun  32792  archirng  33282  archiexdiv  33284  slmdlema  33297  inelcarsg  34489  sibfof  34518  breprexplema  34808  axtgupdim2ALTV  34846  pconncn  35440  ivthALT  36551  poimirlem32  37903  ismtycnv  38053  ismtyima  38054  ismtyres  38059  bfplem1  38073  bfplem2  38074  ghomlinOLD  38139  rngohomadd  38220  rngohommul  38221  crngocom  38252  idladdcl  38270  idllmulcl  38271  idlrmulcl  38272  pridl  38288  ispridlc  38321  pridlc  38322  dmnnzd  38326  oposlem  39558  omllaw  39619  hlsuprexch  39757  lautle  40460  ltrnu  40497  tendovalco  41141  sticksstones1  42516  sticksstones2  42517  ntrkbimka  44394  relprel  45307  mullimc  45976  mullimcf  45983  lptre2pt  45998  fourierdlem54  46518  fcoresf1  47429  faovcl  47560  icceuelpartlem  47795  iccpartnel  47798  fargshiftf1  47801  sprsymrelfolem2  47853  reuopreuprim  47886  isubgr3stgrlem6  48331  isthincd2lem2  49794