Theorem rspc2v 3576

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  rspc2va  3577  rspc3v  3581  rspc6v  3586  disji2  5070  f1veqaeq  7205  isorel  7275  isosolem  7296  oveqrspc2v  7388  fovcld  7488  caovclg  7553  caovcomg  7556  caofidlcan  7663  resf1extb  7879  smoel  8294  fiint  9231  dffi3  9338  ltordlem  11669  seqhomo  14005  cshf1  14766  climcn2  15549  drsdir  18262  tsrlin  18545  dirge  18563  mgmhmlin  18661  issubmgm2  18665  mhmlin  18755  issubg2  19111  nsgbi  19126  ghmlin  19190  efgi  19688  efgred  19717  rglcom4d  20186  irredmul  20403  issubrng2  20529  issubrg2  20563  abvmul  20792  abvtri  20793  lmodlema  20854  islmodd  20855  rmodislmodlem  20918  rmodislmod  20919  lmhmlin  21025  lbsind  21070  rnglidlmcl  21209  ipcj  21627  obsip  21714  mplcoe5lem  22030  matecl  22403  dmatelnd  22474  scmateALT  22490  mdetdiaglem  22576  mdetdiagid  22578  pmatcoe1fsupp  22679  m2cpminvid2lem  22732  inopn  22877  basis1  22928  basis2  22929  iscldtop  23073  hausnei  23306  t1sep2  23347  nconnsubb  23401  r0sep  23726  fbasssin  23814  fcfneii  24015  ustssel  24184  xmeteq0  24316  tngngp3  24634  nmvs  24654  cncfi  24874  c1lip1  25977  aalioulem3  26314  logltb  26580  cvxcl  26965  2sqlem8  27406  nocvxminlem  27763  madebday  27909  negsproplem1  28037  negsprop  28044  axtgcgrrflx  28547  axtgsegcon  28549  axtg5seg  28550  axtgbtwnid  28551  axtgpasch  28552  axtgcont1  28553  axtgupdim2  28556  axtgeucl  28557  isperp2d  28801  f1otrgds  28954  brbtwn2  28991  axcontlem3  29052  axcontlem9  29058  axcontlem10  29059  upgrwlkdvdelem  29822  conngrv2edg  30283  frgrwopreglem5ALT  30410  ablocom  30637  nvs  30752  nvtri  30759  phpar2  30912  phpar  30913  shaddcl  31306  shmulcl  31307  cnopc  32002  unop  32004  hmop  32011  cnfnc  32019  adj1  32022  hstel2  32308  stj  32324  stcltr1i  32363  mddmdin0i  32520  cdj3lem1  32523  cdj3lem2b  32526  disji2f  32665  disjif2  32669  disjxpin  32676  isoun  32793  archirng  33267  archiexdiv  33269  slmdlema  33282  inelcarsg  34474  sibfof  34503  breprexplema  34793  axtgupdim2ALTV  34831  pconncn  35425  ivthALT  36536  poimirlem32  37990  ismtycnv  38140  ismtyima  38141  ismtyres  38146  bfplem1  38160  bfplem2  38161  ghomlinOLD  38226  rngohomadd  38307  rngohommul  38308  crngocom  38339  idladdcl  38357  idllmulcl  38358  idlrmulcl  38359  pridl  38375  ispridlc  38408  pridlc  38409  dmnnzd  38413  oposlem  39645  omllaw  39706  hlsuprexch  39844  lautle  40547  ltrnu  40584  tendovalco  41228  sticksstones1  42602  sticksstones2  42603  ntrkbimka  44486  relprel  45399  mullimc  46067  mullimcf  46074  lptre2pt  46089  fourierdlem54  46609  fcoresf1  47532  faovcl  47663  icceuelpartlem  47910  iccpartnel  47913  fargshiftf1  47916  sprsymrelfolem2  47968  reuopreuprim  48001  isubgr3stgrlem6  48462  isthincd2lem2  49925