Theorem rspc2v 3599

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2va  3600  rspc3v  3604  rspc6v  3609  disji2  5091  f1veqaeq  7231  isorel  7301  isosolem  7322  oveqrspc2v  7414  fovcld  7516  caovclg  7581  caovcomg  7584  caofidlcan  7691  resf1extb  7910  smoel  8329  fiint  9277  fiintOLD  9278  dffi3  9382  ltordlem  11703  seqhomo  14014  cshf1  14775  climcn2  15559  drsdir  18263  tsrlin  18544  dirge  18562  mgmhmlin  18626  issubmgm2  18630  mhmlin  18720  issubg2  19073  nsgbi  19089  ghmlin  19153  efgi  19649  efgred  19678  rglcom4d  20120  irredmul  20338  issubrng2  20467  issubrg2  20501  abvmul  20730  abvtri  20731  lmodlema  20771  islmodd  20772  rmodislmodlem  20835  rmodislmod  20836  lmhmlin  20942  lbsind  20987  rnglidlmcl  21126  ipcj  21543  obsip  21630  mplcoe5lem  21946  matecl  22312  dmatelnd  22383  scmateALT  22399  mdetdiaglem  22485  mdetdiagid  22487  pmatcoe1fsupp  22588  m2cpminvid2lem  22641  inopn  22786  basis1  22837  basis2  22838  iscldtop  22982  hausnei  23215  t1sep2  23256  nconnsubb  23310  r0sep  23635  fbasssin  23723  fcfneii  23924  ustssel  24093  xmeteq0  24226  tngngp3  24544  nmvs  24564  cncfi  24787  c1lip1  25902  aalioulem3  26242  logltb  26509  cvxcl  26895  2sqlem8  27337  nocvxminlem  27689  madebday  27811  negsproplem1  27934  negsprop  27941  axtgcgrrflx  28389  axtgsegcon  28391  axtg5seg  28392  axtgbtwnid  28393  axtgpasch  28394  axtgcont1  28395  axtgupdim2  28398  axtgeucl  28399  isperp2d  28643  f1otrgds  28796  brbtwn2  28832  axcontlem3  28893  axcontlem9  28899  axcontlem10  28900  upgrwlkdvdelem  29666  conngrv2edg  30124  frgrwopreglem5ALT  30251  ablocom  30477  nvs  30592  nvtri  30599  phpar2  30752  phpar  30753  shaddcl  31146  shmulcl  31147  cnopc  31842  unop  31844  hmop  31851  cnfnc  31859  adj1  31862  hstel2  32148  stj  32164  stcltr1i  32203  mddmdin0i  32360  cdj3lem1  32363  cdj3lem2b  32366  disji2f  32506  disjif2  32510  disjxpin  32517  isoun  32625  archirng  33142  archiexdiv  33144  slmdlema  33156  inelcarsg  34302  sibfof  34331  breprexplema  34621  axtgupdim2ALTV  34659  pconncn  35211  ivthALT  36323  poimirlem32  37646  ismtycnv  37796  ismtyima  37797  ismtyres  37802  bfplem1  37816  bfplem2  37817  ghomlinOLD  37882  rngohomadd  37963  rngohommul  37964  crngocom  37995  idladdcl  38013  idllmulcl  38014  idlrmulcl  38015  pridl  38031  ispridlc  38064  pridlc  38065  dmnnzd  38069  oposlem  39175  omllaw  39236  hlsuprexch  39375  lautle  40078  ltrnu  40115  tendovalco  40759  sticksstones1  42134  sticksstones2  42135  ntrkbimka  44027  relprel  44941  mullimc  45614  mullimcf  45621  lptre2pt  45638  fourierdlem54  46158  fcoresf1  47070  faovcl  47201  icceuelpartlem  47436  iccpartnel  47439  fargshiftf1  47442  sprsymrelfolem2  47494  reuopreuprim  47527  isubgr3stgrlem6  47970  isthincd2lem2  49424