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  10622  injresinj  13709  seqcaopr2  13963  rlimcn3  15515  o1of2  15538  isprm6  16643  ssc2  17748  pospropd  18250  tleile  18344  mgmhmpropd  18625  mhmpropd  18719  grpidssd  18948  grpinvssd  18949  dfgrp3lem  18970  isnsg3  19091  cyccom  19134  symgextf1  19352  efgredlemd  19675  efgredlem  19678  rglcom4d  20148  rnghmmul  20387  domneq0  20643  issrngd  20790  orngmul  20800  lindfind  21773  lindsind  21774  mplsubglem  21956  mdetunilem1  22558  mdetunilem3  22560  mdetunilem4  22561  mdetunilem9  22566  decpmatmulsumfsupp  22719  pm2mpf1  22745  pm2mpmhmlem1  22764  t0sep  23270  tsmsxplem2  24100  comet  24459  nrmmetd  24520  tngngp  24600  reconnlem2  24774  iscmet3lem1  25249  iscmet3lem2  25250  dchrisumlem1  27458  pntpbnd1  27555  sltssepc  27769  tgjustc1  28549  tgjustc2  28550  iscgrglt  28588  motcgr  28610  perpneq  28788  foot  28796  f1otrg  28945  axcontlem10  29048  frgr2wwlk1  30406  lindsunlem  33783  mndpluscn  34085  unelros  34330  difelros  34331  inelsros  34337  diffiunisros  34338  elmrsubrn  35716  ghomco  38094  sticksstones10  42431  sticksstones12a  42433  fsuppind  42854  mzpcl34  42994  ntrk0kbimka  44301  isotone1  44310  isotone2  44311  nnfoctbdjlem  46720  2arymaptf1  48920