Theorem rspc 2923

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
rspc.1	⊢ Ⅎ𝑥𝜓
rspc.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspc

Step	Hyp	Ref	Expression
1		df-ral 2533	. 2 ⊢ (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜑))
2		nfcv 2392	. . . 4 ⊢ Ⅎ𝑥𝐴
3		nfv 1581	. . . . 5 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵
4		rspc.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
5	3, 4	nfim 1625	. . . 4 ⊢ Ⅎ𝑥(𝐴 ∈ 𝐵 → 𝜓)
6		eleq1 2301	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
7		rspc.2	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
8	6, 7	imbi12d 234	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 → 𝜑) ↔ (𝐴 ∈ 𝐵 → 𝜓)))
9	2, 5, 8	spcgf 2907	. . 3 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → (𝐴 ∈ 𝐵 → 𝜓)))
10	9	pm2.43a 51	. 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥(𝑥 ∈ 𝐵 → 𝜑) → 𝜓))
11	1, 10	biimtrid 152	1 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wal 1400   = wceq 1402  Ⅎwnf 1513   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823

This theorem is used by:  rspcv  2925  rspc2  2941  rspc2vd  3216  pofun  4459  omsinds  4771  fmptcof  5878  fliftfuns  6007  qliftfuns  6897  xpf1o  7149  finexdc  7212  ssfirab  7249  opabfi  7252  iunfidisj  7265  dcfi  7321  cc3  7641  lble  9286  exfzdc  10677  zsupcllemstep  10680  infssuzex  10684  uzsinds  10903  sumeq2  12151  sumfct  12166  sumrbdclem  12170  summodclem3  12173  summodclem2a  12174  zsumdc  12177  fsumgcl  12179  fsum3  12180  fsumf1o  12183  isumss  12184  isumss2  12186  fsum3cvg2  12187  fsumadd  12199  isummulc2  12219  fsum2dlemstep  12227  fisumcom2  12231  fsumshftm  12238  fisum0diag2  12240  fsummulc2  12241  fsum00  12255  fsumabs  12258  fsumrelem  12264  fsumiun  12270  isumshft  12283  mertenslem2  12329  prodeq2  12350  prodrbdclem  12364  prodmodclem3  12368  prodmodclem2a  12369  zproddc  12372  fprodseq  12376  prodfct  12380  fprodf1o  12381  prodssdc  12382  fprodmul  12384  fprodm1s  12394  fprodp1s  12395  fprodabs  12409  fprodap0  12414  fprod2dlemstep  12415  fprodcom2fi  12419  fprodrec  12422  fprodap0f  12429  fprodle  12433  bezoutlemmain  12801  nnwosdc  12842  pcmpt  13152  ctiunctlemudc  13387  gsummptfidmadd  14252  gsummptfidmsplit  14255  gsumsnfdcmn  14258  idjusnfi  14271  iuncld  15353  txcnp  15509  fsumcncntop  15805  bj-nntrans  17194