Theorem rspc2v 3570

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070

This theorem is referenced by:  rspc2va  3571  rspc3v  3573  disji2  5060  f1veqaeq  7124  isorel  7190  isosolem  7211  oveqrspc2v  7295  fovcl  7393  caovclg  7455  caovcomg  7458  smoel  8175  fiint  9052  dffi3  9151  ltordlem  11483  seqhomo  13751  cshf1  14504  climcn2  15283  drsdir  18001  tsrlin  18284  dirge  18302  mhmlin  18418  issubg2  18751  nsgbi  18766  ghmlin  18820  efgi  19306  efgred  19335  irredmul  19932  issubrg2  20025  abvmul  20070  abvtri  20071  lmodlema  20109  islmodd  20110  rmodislmodlem  20171  rmodislmod  20172  rmodislmodOLD  20173  lmhmlin  20278  lbsind  20323  ipcj  20820  obsip  20909  mplcoe5lem  21221  matecl  21555  dmatelnd  21626  scmateALT  21642  mdetdiaglem  21728  mdetdiagid  21730  pmatcoe1fsupp  21831  m2cpminvid2lem  21884  inopn  22029  basis1  22081  basis2  22082  iscldtop  22227  hausnei  22460  t1sep2  22501  nconnsubb  22555  r0sep  22880  fbasssin  22968  fcfneii  23169  ustssel  23338  xmeteq0  23472  tngngp3  23801  nmvs  23821  cncfi  24038  c1lip1  25142  aalioulem3  25475  logltb  25736  cvxcl  26115  2sqlem8  26555  axtgcgrrflx  26804  axtgsegcon  26806  axtg5seg  26807  axtgbtwnid  26808  axtgpasch  26809  axtgcont1  26810  axtgupdim2  26813  axtgeucl  26814  isperp2d  27058  f1otrgds  27211  brbtwn2  27254  axcontlem3  27315  axcontlem9  27321  axcontlem10  27322  upgrwlkdvdelem  28083  conngrv2edg  28538  frgrwopreglem5ALT  28665  ablocom  28889  nvs  29004  nvtri  29011  phpar2  29164  phpar  29165  shaddcl  29558  shmulcl  29559  cnopc  30254  unop  30256  hmop  30263  cnfnc  30271  adj1  30274  hstel2  30560  stj  30576  stcltr1i  30615  mddmdin0i  30772  cdj3lem1  30775  cdj3lem2b  30778  disji2f  30895  disjif2  30899  disjxpin  30906  fovcld  30954  isoun  31013  archirng  31421  archiexdiv  31423  slmdlema  31435  inelcarsg  32257  sibfof  32286  breprexplema  32589  axtgupdim2ALTV  32627  pconncn  33165  nocvxminlem  33951  madebday  34059  ivthALT  34503  poimirlem32  35788  ismtycnv  35939  ismtyima  35940  ismtyres  35945  bfplem1  35959  bfplem2  35960  ghomlinOLD  36025  rngohomadd  36106  rngohommul  36107  crngocom  36138  idladdcl  36156  idllmulcl  36157  idlrmulcl  36158  pridl  36174  ispridlc  36207  pridlc  36208  dmnnzd  36212  oposlem  37175  omllaw  37236  hlsuprexch  37374  lautle  38077  ltrnu  38114  tendovalco  38758  sticksstones1  40082  sticksstones2  40083  ntrkbimka  41601  mullimc  43111  mullimcf  43118  lptre2pt  43135  fourierdlem54  43655  fcoresf1  44514  faovcl  44643  icceuelpartlem  44839  iccpartnel  44842  fargshiftf1  44845  sprsymrelfolem2  44897  reuopreuprim  44930  mgmhmlin  45292  issubmgm2  45296  isthincd2lem2  46269