Theorem rspc2va 3595

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082

This theorem is used by:  rspc2dv  3598  swopo  5582  f1ounsn  7279  soisores  7334  soisoi  7335  isocnv  7337  isotr  7343  ovrspc2v  7445  coof  7708  caofrss  7723  caonncan  7728  frpoins3xpg  8142  coflton  8663  wunpr  10711  injresinj  13839  seqcaopr2  14094  rlimcn3  15667  o1of2  15690  isprm6  16797  ssc2  17903  pospropd  18405  tleile  18499  mgmhmpropd  18790  mhmpropd  18889  grpidssd  19128  grpinvssd  19129  dfgrp3lem  19150  isnsg3  19272  cyccom  19320  symgextf1  19537  efgredlemd  19860  efgredlem  19863  rglcom4d  20339  rnghmmul  20579  domneq0  20859  issrngd  21010  orngmul  21020  lindfind  22018  lindsind  22019  mplsubglem  22200  mdetunilem1  22821  mdetunilem3  22823  mdetunilem4  22824  mdetunilem9  22829  decpmatmulsumfsupp  22982  pm2mpf1  23008  pm2mpmhmlem1  23027  t0sep  23533  tsmsxplem2  24364  comet  24723  nrmmetd  24784  tngngp  24864  reconnlem2  25038  iscmet3lem1  25503  iscmet3lem2  25504  dchrisumlem1  27706  pntpbnd1  27803  sltssepc  28017  tgjustc1  28797  tgjustc2  28798  iscgrglt  28836  motcgr  28858  perpneq  29047  foot  29055  f1otrg  29277  axcontlem10  29380  frgr2wwlk1  30753  lindsunlem  34080  mndpluscn  34382  unelros  34628  difelros  34629  inelsros  34635  diffiunisros  34636  elmrsubrn  36051  nmuladdel  36743  ghomco  38602  sticksstones10  42982  sticksstones12a  42984  fsuppind  43382  mzpcl34  43522  ntrk0kbimka  44825  isotone1  44834  isotone2  44835  nnfoctbdjlem  47229  2arymaptf1  49492