Theorem rspccv 3579

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.)

Hypothesis

Ref	Expression
rspcv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rspccv	⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspccv

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	rspcv 3578	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))
3	2	com12 32	1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061

This theorem is referenced by:  elinti  4921  trss  5238  fvn0ssdmfun  7030  dff3  7055  2fvcoidd  7248  ofrval  7634  limsuc  7790  limuni3  7793  peano5  7835  frxp  8063  wfrdmclOLD  8268  smo11  8315  odi  8531  supub  9404  suplub  9405  elirrv  9541  dfom3  9592  noinfep  9605  tcrank  9829  alephle  10033  dfac5lem5  10072  dfac2b  10075  cofsmo  10214  coftr  10218  infpssrlem4  10251  isf34lem6  10325  axcc2lem  10381  domtriomlem  10387  axdc2lem  10393  axdc3lem2  10396  axdc4lem  10400  ac5b  10423  zorn2lem2  10442  zorn2lem6  10446  pwcfsdom  10528  inar1  10720  grupw  10740  grupr  10742  gruurn  10743  grothpw  10771  grothpwex  10772  axgroth6  10773  grothomex  10774  nqereu  10874  supsrlem  11056  axpre-sup  11114  dedekind  11327  dedekindle  11328  supmullem1  12134  supmul  12136  peano5nni  12165  dfnn2  12175  peano5uzi  12601  zindd  12613  lcmfdvds  16529  lcmfunsn  16531  1arith  16810  ramcl  16912  clatleglb  18421  pslem  18475  cyccom  19010  psgndiflemA  21042  eqcoe1ply1eq  21705  mvmumamul1  21940  smadiadetlem0  22047  chpscmat  22228  basis2  22338  tg2  22352  clsndisj  22463  cnpimaex  22644  t1sncld  22714  regsep  22722  nrmsep3  22743  cmpsub  22788  2ndc1stc  22839  refssex  22899  ptfinfin  22907  txcnpi  22996  txcmplem1  23029  tx1stc  23038  filss  23241  ufilss  23293  fclsopni  23403  fclsrest  23412  alexsubb  23434  alexsubALTlem2  23436  alexsubALTlem4  23438  ghmcnp  23503  qustgplem  23509  mopni  23885  metrest  23917  metcnpi  23937  metcnpi2  23938  nmolb  24118  nmoleub2lem2  24516  ovoliunlem1  24903  ovolicc2lem3  24920  mblsplit  24933  fta1b  25571  plycj  25675  lgamgulmlem1  26415  sqfpc  26523  ostth2lem2  27019  ostth3  27023  sltval2  27041  nogt01o  27081  madebdayim  27260  madebdaylemlrcut  27271  vdiscusgr  28542  0vtxrusgr  28588  rusgrnumwrdl2  28597  ewlkinedg  28615  eupthseg  29213  upgreupthseg  29216  numclwwlk1  29368  l2p  29484  lpni  29485  nvz  29674  chcompl  30247  ocin  30301  hmopidmchi  31156  dmdmd  31305  dmdbr5  31313  mdsl1i  31326  sigaclci  32820  bnj23  33419  kur14lem9  33895  sconnpht  33910  cvmsdisj  33951  sat1el2xp  34060  untelirr  34366  untsucf  34368  dfon2lem4  34447  dfon2lem6  34449  dfon2lem7  34450  dfon2lem8  34451  dfon2  34453  fwddifnp1  34826  domalom  35948  pibt2  35961  poimirlem18  36169  poimirlem21  36172  heibor1lem  36341  heiborlem4  36346  heiborlem6  36348  atlex  37851  psubspi  38283  elpcliN  38429  ldilval  38649  trlord  39105  tendotp  39297  hdmapval2  40368  cantnfresb  41717  pwelg  41954  gneispace0nelrn2  42535  gneispaceel2  42538  gneispacess2  42540  stoweid  44424  iccpartimp  45729  iccpartltu  45737  iccpartgtl  45738  iccpartleu  45740  iccpartgel  45741  isomushgr  46138  isomuspgrlem1  46139  isomuspgr  46146  isomgrtrlem  46150  1arymaptf1  46848