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 412	1 ⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑) → 𝜓)

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  rspc2dv  3591  swopo  5570  f1ounsn  7280  soisores  7335  soisoi  7336  isocnv  7338  isotr  7344  ovrspc2v  7446  coof  7717  caofrss  7732  caonncan  7737  frpoins3xpg  8157  coflton  8680  wunpr  10794  injresinj  13926  seqcaopr2  14181  rlimcn3  15757  o1of2  15780  isprm6  16890  ssc2  17997  pospropd  18499  tleile  18593  mgmhmpropd  18887  mhmpropd  18987  grpidssd  19226  grpinvssd  19227  dfgrp3lem  19248  isnsg3  19370  cyccom  19418  symgextf1  19635  efgredlemd  19958  efgredlem  19961  rglcom4d  20437  rnghmmul  20679  domneq0  20960  issrngd  21112  orngmul  21122  lindfind  22122  lindsind  22123  mplsubglem  22306  mdetunilem1  22927  mdetunilem3  22929  mdetunilem4  22930  mdetunilem9  22935  decpmatmulsumfsupp  23091  pm2mpf1  23117  pm2mpmhmlem1  23136  t0sep  23642  tsmsxplem2  24473  comet  24832  nrmmetd  24893  tngngp  24973  reconnlem2  25147  iscmet3lem1  25612  iscmet3lem2  25613  dchrisumlem1  27816  pntpbnd1  27913  sltssepc  28157  tgjustc1  28937  tgjustc2  28938  iscgrglt  28977  motcgr  28999  perpneq  29189  foot  29197  f1otrg  29448  axcontlem10  29551  frgr2wwlk1  30930  lindsunlem  34256  mndpluscn  34558  unelros  34804  difelros  34805  inelsros  34811  diffiunisros  34812  elmrsubrn  36285  nmuladdel  36961  ghomco  38825  sticksstones10  43205  sticksstones12a  43207  fsuppind  43618  mzpcl34  43741  ntrk0kbimka  45038  isotone1  45047  isotone2  45048  nnfoctbdjlem  47464  2arymaptf1  49764