Theorem rspc2va 3589

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  rspc2dv  3592  swopo  5538  f1ounsn  7209  soisores  7264  soisoi  7265  isocnv  7267  isotr  7273  ovrspc2v  7375  coof  7637  caofrss  7652  caonncan  7657  frpoins3xpg  8073  coflton  8589  wunpr  10603  injresinj  13691  seqcaopr2  13945  rlimcn3  15497  o1of2  15520  isprm6  16625  ssc2  17729  pospropd  18231  tleile  18325  mgmhmpropd  18572  mhmpropd  18666  grpidssd  18895  grpinvssd  18896  dfgrp3lem  18917  isnsg3  19039  cyccom  19082  symgextf1  19300  efgredlemd  19623  efgredlem  19626  rglcom4d  20096  rnghmmul  20334  domneq0  20593  issrngd  20740  orngmul  20750  lindfind  21723  lindsind  21724  mplsubglem  21906  mdetunilem1  22497  mdetunilem3  22499  mdetunilem4  22500  mdetunilem9  22505  decpmatmulsumfsupp  22658  pm2mpf1  22684  pm2mpmhmlem1  22703  t0sep  23209  tsmsxplem2  24039  comet  24399  nrmmetd  24460  tngngp  24540  reconnlem2  24714  iscmet3lem1  25189  iscmet3lem2  25190  dchrisumlem1  27398  pntpbnd1  27495  ssltsepc  27704  tgjustc1  28420  tgjustc2  28421  iscgrglt  28459  motcgr  28481  perpneq  28659  foot  28667  f1otrg  28816  axcontlem10  28918  frgr2wwlk1  30273  lindsunlem  33597  mndpluscn  33899  unelros  34144  difelros  34145  inelsros  34151  diffiunisros  34152  elmrsubrn  35503  ghomco  37881  sticksstones10  42138  sticksstones12a  42140  fsuppind  42573  mzpcl34  42714  ntrk0kbimka  44022  isotone1  44031  isotone2  44032  nnfoctbdjlem  46446  2arymaptf1  48648