Theorem rspc2v 3587

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspc2va  3588  rspc3v  3592  rspc6v  3597  disji2  5082  f1veqaeq  7202  isorel  7272  isosolem  7293  oveqrspc2v  7385  fovcld  7485  caovclg  7550  caovcomg  7553  caofidlcan  7660  resf1extb  7876  smoel  8292  fiint  9227  dffi3  9334  ltordlem  11662  seqhomo  13972  cshf1  14733  climcn2  15516  drsdir  18225  tsrlin  18508  dirge  18526  mgmhmlin  18624  issubmgm2  18628  mhmlin  18718  issubg2  19071  nsgbi  19086  ghmlin  19150  efgi  19648  efgred  19677  rglcom4d  20146  irredmul  20365  issubrng2  20491  issubrg2  20525  abvmul  20754  abvtri  20755  lmodlema  20816  islmodd  20817  rmodislmodlem  20880  rmodislmod  20881  lmhmlin  20987  lbsind  21032  rnglidlmcl  21171  ipcj  21589  obsip  21676  mplcoe5lem  21994  matecl  22369  dmatelnd  22440  scmateALT  22456  mdetdiaglem  22542  mdetdiagid  22544  pmatcoe1fsupp  22645  m2cpminvid2lem  22698  inopn  22843  basis1  22894  basis2  22895  iscldtop  23039  hausnei  23272  t1sep2  23313  nconnsubb  23367  r0sep  23692  fbasssin  23780  fcfneii  23981  ustssel  24150  xmeteq0  24282  tngngp3  24600  nmvs  24620  cncfi  24843  c1lip1  25958  aalioulem3  26298  logltb  26565  cvxcl  26951  2sqlem8  27393  nocvxminlem  27750  madebday  27896  negsproplem1  28024  negsprop  28031  axtgcgrrflx  28534  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  axtgupdim2  28543  axtgeucl  28544  isperp2d  28788  f1otrgds  28941  brbtwn2  28978  axcontlem3  29039  axcontlem9  29045  axcontlem10  29046  upgrwlkdvdelem  29809  conngrv2edg  30270  frgrwopreglem5ALT  30397  ablocom  30623  nvs  30738  nvtri  30745  phpar2  30898  phpar  30899  shaddcl  31292  shmulcl  31293  cnopc  31988  unop  31990  hmop  31997  cnfnc  32005  adj1  32008  hstel2  32294  stj  32310  stcltr1i  32349  mddmdin0i  32506  cdj3lem1  32509  cdj3lem2b  32512  disji2f  32652  disjif2  32656  disjxpin  32663  isoun  32781  archirng  33270  archiexdiv  33272  slmdlema  33285  inelcarsg  34468  sibfof  34497  breprexplema  34787  axtgupdim2ALTV  34825  pconncn  35418  ivthALT  36529  poimirlem32  37853  ismtycnv  38003  ismtyima  38004  ismtyres  38009  bfplem1  38023  bfplem2  38024  ghomlinOLD  38089  rngohomadd  38170  rngohommul  38171  crngocom  38202  idladdcl  38220  idllmulcl  38221  idlrmulcl  38222  pridl  38238  ispridlc  38271  pridlc  38272  dmnnzd  38276  oposlem  39452  omllaw  39513  hlsuprexch  39651  lautle  40354  ltrnu  40391  tendovalco  41035  sticksstones1  42410  sticksstones2  42411  ntrkbimka  44289  relprel  45202  mullimc  45872  mullimcf  45879  lptre2pt  45894  fourierdlem54  46414  fcoresf1  47325  faovcl  47456  icceuelpartlem  47691  iccpartnel  47694  fargshiftf1  47697  sprsymrelfolem2  47749  reuopreuprim  47782  isubgr3stgrlem6  48227  isthincd2lem2  49690