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 3076

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  rspc2dv  3591  swopo  5574  f1ounsn  7274  soisores  7329  soisoi  7330  isocnv  7332  isotr  7338  ovrspc2v  7440  coof  7703  caofrss  7718  caonncan  7723  frpoins3xpg  8139  coflton  8662  wunpr  10721  injresinj  13850  seqcaopr2  14105  rlimcn3  15680  o1of2  15703  isprm6  16808  ssc2  17914  pospropd  18416  tleile  18510  mgmhmpropd  18803  mhmpropd  18903  grpidssd  19142  grpinvssd  19143  dfgrp3lem  19164  isnsg3  19286  cyccom  19334  symgextf1  19551  efgredlemd  19874  efgredlem  19877  rglcom4d  20353  rnghmmul  20593  domneq0  20873  issrngd  21024  orngmul  21034  lindfind  22032  lindsind  22033  mplsubglem  22216  mdetunilem1  22837  mdetunilem3  22839  mdetunilem4  22840  mdetunilem9  22845  decpmatmulsumfsupp  23001  pm2mpf1  23027  pm2mpmhmlem1  23046  t0sep  23552  tsmsxplem2  24383  comet  24742  nrmmetd  24803  tngngp  24883  reconnlem2  25057  iscmet3lem1  25522  iscmet3lem2  25523  dchrisumlem1  27728  pntpbnd1  27825  sltssepc  28039  tgjustc1  28819  tgjustc2  28820  iscgrglt  28859  motcgr  28881  perpneq  29071  foot  29079  f1otrg  29330  axcontlem10  29433  frgr2wwlk1  30812  lindsunlem  34137  mndpluscn  34439  unelros  34685  difelros  34686  inelsros  34692  diffiunisros  34693  elmrsubrn  36102  nmuladdel  36795  ghomco  38644  sticksstones10  43024  sticksstones12a  43026  fsuppind  43439  mzpcl34  43579  ntrk0kbimka  44882  isotone1  44891  isotone2  44892  nnfoctbdjlem  47286  2arymaptf1  49586