Theorem rspc2va 3603

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  rspc2dv  3606  swopo  5560  f1ounsn  7250  soisores  7305  soisoi  7306  isocnv  7308  isotr  7314  ovrspc2v  7416  coof  7680  caofrss  7695  caonncan  7700  frpoins3xpg  8122  coflton  8638  wunpr  10669  injresinj  13756  seqcaopr2  14010  rlimcn3  15563  o1of2  15586  isprm6  16691  ssc2  17791  pospropd  18293  tleile  18387  mgmhmpropd  18632  mhmpropd  18726  grpidssd  18955  grpinvssd  18956  dfgrp3lem  18977  isnsg3  19099  cyccom  19142  symgextf1  19358  efgredlemd  19681  efgredlem  19684  rglcom4d  20127  rnghmmul  20365  domneq0  20624  issrngd  20771  lindfind  21732  lindsind  21733  mplsubglem  21915  mdetunilem1  22506  mdetunilem3  22508  mdetunilem4  22509  mdetunilem9  22514  decpmatmulsumfsupp  22667  pm2mpf1  22693  pm2mpmhmlem1  22712  t0sep  23218  tsmsxplem2  24048  comet  24408  nrmmetd  24469  tngngp  24549  reconnlem2  24723  iscmet3lem1  25198  iscmet3lem2  25199  dchrisumlem1  27407  pntpbnd1  27504  ssltsepc  27712  tgjustc1  28409  tgjustc2  28410  iscgrglt  28448  motcgr  28470  perpneq  28648  foot  28656  f1otrg  28805  axcontlem10  28907  frgr2wwlk1  30265  orngmul  33288  lindsunlem  33627  mndpluscn  33923  unelros  34168  difelros  34169  inelsros  34175  diffiunisros  34176  elmrsubrn  35514  ghomco  37892  sticksstones10  42150  sticksstones12a  42152  fsuppind  42585  mzpcl34  42726  ntrk0kbimka  44035  isotone1  44044  isotone2  44045  nnfoctbdjlem  46460  2arymaptf1  48646