Theorem rspc2va 3586

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 3585	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓))
4	3	imp 406	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050

This theorem is referenced by:  rspc2dv  3589  swopo  5541  f1ounsn  7216  soisores  7271  soisoi  7272  isocnv  7274  isotr  7280  ovrspc2v  7382  coof  7644  caofrss  7659  caonncan  7664  frpoins3xpg  8080  coflton  8597  wunpr  10618  injresinj  13705  seqcaopr2  13959  rlimcn3  15511  o1of2  15534  isprm6  16639  ssc2  17744  pospropd  18246  tleile  18340  mgmhmpropd  18621  mhmpropd  18715  grpidssd  18944  grpinvssd  18945  dfgrp3lem  18966  isnsg3  19087  cyccom  19130  symgextf1  19348  efgredlemd  19671  efgredlem  19674  rglcom4d  20144  rnghmmul  20383  domneq0  20639  issrngd  20786  orngmul  20796  lindfind  21769  lindsind  21770  mplsubglem  21952  mdetunilem1  22554  mdetunilem3  22556  mdetunilem4  22557  mdetunilem9  22562  decpmatmulsumfsupp  22715  pm2mpf1  22741  pm2mpmhmlem1  22760  t0sep  23266  tsmsxplem2  24096  comet  24455  nrmmetd  24516  tngngp  24596  reconnlem2  24770  iscmet3lem1  25245  iscmet3lem2  25246  dchrisumlem1  27454  pntpbnd1  27551  ssltsepc  27761  tgjustc1  28496  tgjustc2  28497  iscgrglt  28535  motcgr  28557  perpneq  28735  foot  28743  f1otrg  28892  axcontlem10  28995  frgr2wwlk1  30353  lindsunlem  33730  mndpluscn  34032  unelros  34277  difelros  34278  inelsros  34284  diffiunisros  34285  elmrsubrn  35663  ghomco  38031  sticksstones10  42348  sticksstones12a  42350  fsuppind  42775  mzpcl34  42915  ntrk0kbimka  44222  isotone1  44231  isotone2  44232  nnfoctbdjlem  46641  2arymaptf1  48841