Theorem rspc2va 3591

Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 18-Jun-2014.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2va	⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2va

Step	Hyp	Ref	Expression
1		rspc2v.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		rspc2v.2	. . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
3	1, 2	rspc2v 3590	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 412	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079

This theorem is used by:  rspc2dv  3594  swopo  5578  f1ounsn  7277  soisores  7332  soisoi  7333  isocnv  7335  isotr  7341  ovrspc2v  7443  coof  7706  caofrss  7721  caonncan  7726  frpoins3xpg  8142  coflton  8663  wunpr  10722  injresinj  13851  seqcaopr2  14106  rlimcn3  15681  o1of2  15704  isprm6  16811  ssc2  17917  pospropd  18419  tleile  18513  mgmhmpropd  18806  mhmpropd  18906  grpidssd  19145  grpinvssd  19146  dfgrp3lem  19167  isnsg3  19289  cyccom  19337  symgextf1  19554  efgredlemd  19877  efgredlem  19880  rglcom4d  20356  rnghmmul  20596  domneq0  20876  issrngd  21027  orngmul  21037  lindfind  22035  lindsind  22036  mplsubglem  22219  mdetunilem1  22840  mdetunilem3  22842  mdetunilem4  22843  mdetunilem9  22848  decpmatmulsumfsupp  23004  pm2mpf1  23030  pm2mpmhmlem1  23049  t0sep  23555  tsmsxplem2  24386  comet  24745  nrmmetd  24806  tngngp  24886  reconnlem2  25060  iscmet3lem1  25525  iscmet3lem2  25526  dchrisumlem1  27733  pntpbnd1  27830  sltssepc  28044  tgjustc1  28824  tgjustc2  28825  iscgrglt  28864  motcgr  28886  perpneq  29076  foot  29084  f1otrg  29335  axcontlem10  29438  frgr2wwlk1  30817  lindsunlem  34142  mndpluscn  34444  unelros  34690  difelros  34691  inelsros  34697  diffiunisros  34698  elmrsubrn  36107  nmuladdel  36800  ghomco  38649  sticksstones10  43029  sticksstones12a  43031  fsuppind  43444  mzpcl34  43584  ntrk0kbimka  44887  isotone1  44896  isotone2  44897  nnfoctbdjlem  47291  2arymaptf1  49591