Theorem ralrab 3641

Description: Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.)

Hypothesis

Ref	Expression
ralab.1	⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralrab	⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))

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

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralrab

Step	Hyp	Ref	Expression
1		ralab.1	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓))
2	1	elrab 3635	. . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	imbi1i 349	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
4		impexp 450	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	3, 4	bitri 275	. 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
6	5	ralbii2 3080	1 ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∀wral 3052  {crab 3390

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3391  df-v 3432

This theorem is referenced by:  frminex  5604  wereu2  5622  frpomin  6299  weniso  7303  zmin  12888  prmreclem1  16881  lublecllem  18318  mgmhmeql  18678  mhmeql  18788  ghmeql  19208  pgpfac1lem5  20050  lmhmeql  21045  islindf4  21831  1stcfb  23423  fbssfi  23815  filssufilg  23889  txflf  23984  ptcmplem3  24032  symgtgp  24084  tgpconncompeqg  24090  cnllycmp  24936  ovolgelb  25460  dyadmax  25578  lhop1  25994  radcnvlt1  26399  noextenddif  27649  conway  27788  madebdaylemlrcut  27908  oncutlt  28273  oniso  28280  bdayons  28285  bdayn0p1  28378  poimirlem4  37962  poimirlem32  37990  ismblfin  37999  igenval2  38404  glbconN  39840  nadd2rabtr  43833  isubgruhgr  48359  intubeu  49474  unilbeu  49475