Theorem rspc2va 3588

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  rspc2dv  3591  swopo  5543  f1ounsn  7218  soisores  7273  soisoi  7274  isocnv  7276  isotr  7282  ovrspc2v  7384  coof  7646  caofrss  7661  caonncan  7666  frpoins3xpg  8082  coflton  8599  wunpr  10620  injresinj  13707  seqcaopr2  13961  rlimcn3  15513  o1of2  15536  isprm6  16641  ssc2  17746  pospropd  18248  tleile  18342  mgmhmpropd  18623  mhmpropd  18717  grpidssd  18946  grpinvssd  18947  dfgrp3lem  18968  isnsg3  19089  cyccom  19132  symgextf1  19350  efgredlemd  19673  efgredlem  19676  rglcom4d  20146  rnghmmul  20385  domneq0  20641  issrngd  20788  orngmul  20798  lindfind  21771  lindsind  21772  mplsubglem  21954  mdetunilem1  22556  mdetunilem3  22558  mdetunilem4  22559  mdetunilem9  22564  decpmatmulsumfsupp  22717  pm2mpf1  22743  pm2mpmhmlem1  22762  t0sep  23268  tsmsxplem2  24098  comet  24457  nrmmetd  24518  tngngp  24598  reconnlem2  24772  iscmet3lem1  25247  iscmet3lem2  25248  dchrisumlem1  27456  pntpbnd1  27553  sltssepc  27767  tgjustc1  28547  tgjustc2  28548  iscgrglt  28586  motcgr  28608  perpneq  28786  foot  28794  f1otrg  28943  axcontlem10  29046  frgr2wwlk1  30404  lindsunlem  33781  mndpluscn  34083  unelros  34328  difelros  34329  inelsros  34335  diffiunisros  34336  elmrsubrn  35714  ghomco  38092  sticksstones10  42409  sticksstones12a  42411  fsuppind  42833  mzpcl34  42973  ntrk0kbimka  44280  isotone1  44289  isotone2  44290  nnfoctbdjlem  46699  2arymaptf1  48899