Theorem rspc2va 3572

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054

This theorem is referenced by:  rspc2dv  3575  swopo  5537  f1ounsn  7216  soisores  7271  soisoi  7272  isocnv  7274  isotr  7280  ovrspc2v  7382  coof  7644  caofrss  7659  caonncan  7664  frpoins3xpg  8080  coflton  8597  wunpr  10623  injresinj  13737  seqcaopr2  13991  rlimcn3  15543  o1of2  15566  isprm6  16675  ssc2  17780  pospropd  18282  tleile  18376  mgmhmpropd  18657  mhmpropd  18751  grpidssd  18983  grpinvssd  18984  dfgrp3lem  19005  isnsg3  19126  cyccom  19169  symgextf1  19387  efgredlemd  19710  efgredlem  19713  rglcom4d  20183  rnghmmul  20420  domneq0  20680  issrngd  20827  orngmul  20837  lindfind  21791  lindsind  21792  mplsubglem  21973  mdetunilem1  22595  mdetunilem3  22597  mdetunilem4  22598  mdetunilem9  22603  decpmatmulsumfsupp  22756  pm2mpf1  22782  pm2mpmhmlem1  22801  t0sep  23307  tsmsxplem2  24137  comet  24496  nrmmetd  24557  tngngp  24637  reconnlem2  24811  iscmet3lem1  25276  iscmet3lem2  25277  dchrisumlem1  27470  pntpbnd1  27567  sltssepc  27781  tgjustc1  28561  tgjustc2  28562  iscgrglt  28600  motcgr  28622  perpneq  28800  foot  28808  f1otrg  28957  axcontlem10  29060  frgr2wwlk1  30417  lindsunlem  33808  mndpluscn  34110  unelros  34355  difelros  34356  inelsros  34362  diffiunisros  34363  elmrsubrn  35748  ghomco  38258  sticksstones10  42640  sticksstones12a  42642  fsuppind  43040  mzpcl34  43180  ntrk0kbimka  44483  isotone1  44492  isotone2  44493  nnfoctbdjlem  46898  2arymaptf1  49144