Theorem rspc2v 3575

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  ∀wral 3062

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063

This theorem is referenced by:  rspc2va  3576  rspc3v  3578  disji2  5063  f1veqaeq  7162  isorel  7229  isosolem  7250  oveqrspc2v  7334  fovcl  7434  caovclg  7496  caovcomg  7499  smoel  8222  fiint  9135  dffi3  9234  ltordlem  11546  seqhomo  13816  cshf1  14568  climcn2  15347  drsdir  18065  tsrlin  18348  dirge  18366  mhmlin  18482  issubg2  18815  nsgbi  18830  ghmlin  18884  efgi  19370  efgred  19399  irredmul  19996  issubrg2  20089  abvmul  20134  abvtri  20135  lmodlema  20173  islmodd  20174  rmodislmodlem  20235  rmodislmod  20236  rmodislmodOLD  20237  lmhmlin  20342  lbsind  20387  ipcj  20884  obsip  20973  mplcoe5lem  21285  matecl  21619  dmatelnd  21690  scmateALT  21706  mdetdiaglem  21792  mdetdiagid  21794  pmatcoe1fsupp  21895  m2cpminvid2lem  21948  inopn  22093  basis1  22145  basis2  22146  iscldtop  22291  hausnei  22524  t1sep2  22565  nconnsubb  22619  r0sep  22944  fbasssin  23032  fcfneii  23233  ustssel  23402  xmeteq0  23536  tngngp3  23865  nmvs  23885  cncfi  24102  c1lip1  25206  aalioulem3  25539  logltb  25800  cvxcl  26179  2sqlem8  26619  axtgcgrrflx  26868  axtgsegcon  26870  axtg5seg  26871  axtgbtwnid  26872  axtgpasch  26873  axtgcont1  26874  axtgupdim2  26877  axtgeucl  26878  isperp2d  27122  f1otrgds  27275  brbtwn2  27318  axcontlem3  27379  axcontlem9  27385  axcontlem10  27386  upgrwlkdvdelem  28149  conngrv2edg  28604  frgrwopreglem5ALT  28731  ablocom  28955  nvs  29070  nvtri  29077  phpar2  29230  phpar  29231  shaddcl  29624  shmulcl  29625  cnopc  30320  unop  30322  hmop  30329  cnfnc  30337  adj1  30340  hstel2  30626  stj  30642  stcltr1i  30681  mddmdin0i  30838  cdj3lem1  30841  cdj3lem2b  30844  disji2f  30961  disjif2  30965  disjxpin  30972  fovcld  31020  isoun  31079  archirng  31487  archiexdiv  31489  slmdlema  31501  inelcarsg  32323  sibfof  32352  breprexplema  32655  axtgupdim2ALTV  32693  pconncn  33231  nocvxminlem  34017  madebday  34125  ivthALT  34569  poimirlem32  35853  ismtycnv  36004  ismtyima  36005  ismtyres  36010  bfplem1  36024  bfplem2  36025  ghomlinOLD  36090  rngohomadd  36171  rngohommul  36172  crngocom  36203  idladdcl  36221  idllmulcl  36222  idlrmulcl  36223  pridl  36239  ispridlc  36272  pridlc  36273  dmnnzd  36277  oposlem  37238  omllaw  37299  hlsuprexch  37437  lautle  38140  ltrnu  38177  tendovalco  38821  sticksstones1  40144  sticksstones2  40145  ntrkbimka  41686  mullimc  43206  mullimcf  43213  lptre2pt  43230  fourierdlem54  43750  fcoresf1  44621  faovcl  44750  icceuelpartlem  44945  iccpartnel  44948  fargshiftf1  44951  sprsymrelfolem2  45003  reuopreuprim  45036  mgmhmlin  45398  issubmgm2  45402  isthincd2lem2  46375