Theorem rspc2v 3646

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  rspc2va  3647  rspc3v  3651  rspc6v  3656  disji2  5150  f1veqaeq  7294  isorel  7362  isosolem  7383  oveqrspc2v  7475  fovcld  7577  caovclg  7642  caovcomg  7645  smoel  8416  fiint  9394  fiintOLD  9395  dffi3  9500  ltordlem  11815  seqhomo  14100  cshf1  14858  climcn2  15639  drsdir  18372  tsrlin  18655  dirge  18673  mgmhmlin  18737  issubmgm2  18741  mhmlin  18828  issubg2  19181  nsgbi  19197  ghmlin  19261  efgi  19761  efgred  19790  rglcom4d  20238  irredmul  20455  issubrng2  20584  issubrg2  20620  abvmul  20844  abvtri  20845  lmodlema  20885  islmodd  20886  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lmhmlin  21057  lbsind  21102  rnglidlmcl  21249  ipcj  21675  obsip  21764  mplcoe5lem  22080  matecl  22452  dmatelnd  22523  scmateALT  22539  mdetdiaglem  22625  mdetdiagid  22627  pmatcoe1fsupp  22728  m2cpminvid2lem  22781  inopn  22926  basis1  22978  basis2  22979  iscldtop  23124  hausnei  23357  t1sep2  23398  nconnsubb  23452  r0sep  23777  fbasssin  23865  fcfneii  24066  ustssel  24235  xmeteq0  24369  tngngp3  24698  nmvs  24718  cncfi  24939  c1lip1  26056  aalioulem3  26394  logltb  26660  cvxcl  27046  2sqlem8  27488  nocvxminlem  27840  madebday  27956  negsproplem1  28078  negsprop  28085  axtgcgrrflx  28488  axtgsegcon  28490  axtg5seg  28491  axtgbtwnid  28492  axtgpasch  28493  axtgcont1  28494  axtgupdim2  28497  axtgeucl  28498  isperp2d  28742  f1otrgds  28895  brbtwn2  28938  axcontlem3  28999  axcontlem9  29005  axcontlem10  29006  upgrwlkdvdelem  29772  conngrv2edg  30227  frgrwopreglem5ALT  30354  ablocom  30580  nvs  30695  nvtri  30702  phpar2  30855  phpar  30856  shaddcl  31249  shmulcl  31250  cnopc  31945  unop  31947  hmop  31954  cnfnc  31962  adj1  31965  hstel2  32251  stj  32267  stcltr1i  32306  mddmdin0i  32463  cdj3lem1  32466  cdj3lem2b  32469  disji2f  32599  disjif2  32603  disjxpin  32610  isoun  32713  archirng  33168  archiexdiv  33170  slmdlema  33182  inelcarsg  34276  sibfof  34305  breprexplema  34607  axtgupdim2ALTV  34645  pconncn  35192  ivthALT  36301  poimirlem32  37612  ismtycnv  37762  ismtyima  37763  ismtyres  37768  bfplem1  37782  bfplem2  37783  ghomlinOLD  37848  rngohomadd  37929  rngohommul  37930  crngocom  37961  idladdcl  37979  idllmulcl  37980  idlrmulcl  37981  pridl  37997  ispridlc  38030  pridlc  38031  dmnnzd  38035  oposlem  39138  omllaw  39199  hlsuprexch  39338  lautle  40041  ltrnu  40078  tendovalco  40722  sticksstones1  42103  sticksstones2  42104  ntrkbimka  44000  mullimc  45537  mullimcf  45544  lptre2pt  45561  fourierdlem54  46081  fcoresf1  46984  faovcl  47115  icceuelpartlem  47309  iccpartnel  47312  fargshiftf1  47315  sprsymrelfolem2  47367  reuopreuprim  47400  isthincd2lem2  48703