Theorem rspc2v 3623

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

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

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060

This theorem is referenced by:  rspc2va  3624  rspc3v  3628  rspc6v  3632  disji2  5131  f1veqaeq  7260  isorel  7327  isosolem  7348  oveqrspc2v  7440  fovcld  7540  caovclg  7603  caovcomg  7606  smoel  8364  fiint  9328  dffi3  9430  ltordlem  11745  seqhomo  14021  cshf1  14766  climcn2  15543  drsdir  18261  tsrlin  18544  dirge  18562  mgmhmlin  18626  issubmgm2  18630  mhmlin  18717  issubg2  19059  nsgbi  19075  ghmlin  19137  efgi  19630  efgred  19659  rglcom4d  20107  irredmul  20322  issubrng2  20448  issubrg2  20484  abvmul  20582  abvtri  20583  lmodlema  20621  islmodd  20622  rmodislmodlem  20685  rmodislmod  20686  rmodislmodOLD  20687  lmhmlin  20792  lbsind  20837  rnglidlmcl  20984  ipcj  21408  obsip  21497  mplcoe5lem  21815  matecl  22149  dmatelnd  22220  scmateALT  22236  mdetdiaglem  22322  mdetdiagid  22324  pmatcoe1fsupp  22425  m2cpminvid2lem  22478  inopn  22623  basis1  22675  basis2  22676  iscldtop  22821  hausnei  23054  t1sep2  23095  nconnsubb  23149  r0sep  23474  fbasssin  23562  fcfneii  23763  ustssel  23932  xmeteq0  24066  tngngp3  24395  nmvs  24415  cncfi  24636  c1lip1  25748  aalioulem3  26081  logltb  26342  cvxcl  26723  2sqlem8  27163  nocvxminlem  27513  madebday  27629  negsproplem1  27739  negsprop  27746  axtgcgrrflx  27978  axtgsegcon  27980  axtg5seg  27981  axtgbtwnid  27982  axtgpasch  27983  axtgcont1  27984  axtgupdim2  27987  axtgeucl  27988  isperp2d  28232  f1otrgds  28385  brbtwn2  28428  axcontlem3  28489  axcontlem9  28495  axcontlem10  28496  upgrwlkdvdelem  29258  conngrv2edg  29713  frgrwopreglem5ALT  29840  ablocom  30066  nvs  30181  nvtri  30188  phpar2  30341  phpar  30342  shaddcl  30735  shmulcl  30736  cnopc  31431  unop  31433  hmop  31440  cnfnc  31448  adj1  31451  hstel2  31737  stj  31753  stcltr1i  31792  mddmdin0i  31949  cdj3lem1  31952  cdj3lem2b  31955  disji2f  32073  disjif2  32077  disjxpin  32084  isoun  32188  archirng  32602  archiexdiv  32604  slmdlema  32616  inelcarsg  33606  sibfof  33635  breprexplema  33938  axtgupdim2ALTV  33976  pconncn  34511  ivthALT  35525  poimirlem32  36825  ismtycnv  36975  ismtyima  36976  ismtyres  36981  bfplem1  36995  bfplem2  36996  ghomlinOLD  37061  rngohomadd  37142  rngohommul  37143  crngocom  37174  idladdcl  37192  idllmulcl  37193  idlrmulcl  37194  pridl  37210  ispridlc  37243  pridlc  37244  dmnnzd  37248  oposlem  38357  omllaw  38418  hlsuprexch  38557  lautle  39260  ltrnu  39297  tendovalco  39941  sticksstones1  41270  sticksstones2  41271  ntrkbimka  43093  mullimc  44632  mullimcf  44639  lptre2pt  44656  fourierdlem54  45176  fcoresf1  46079  faovcl  46208  icceuelpartlem  46403  iccpartnel  46406  fargshiftf1  46409  sprsymrelfolem2  46461  reuopreuprim  46494  isthincd2lem2  47745