Theorem ralrab 3657

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 3650	. . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	imbi1i 352	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
4		impexp 455	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	3, 4	bitri 278	. 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
6	5	ralbii2 3107	1 ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ∀wral 3079  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rab 3417  df-v 3457

This theorem is referenced by:  frminex  5640  wereu2  5658  frpomin  6341  weniso  7352  zmin  12963  prmreclem1  16971  lublecllem  18409  mgmhmeql  18769  mhmeql  18880  ghmeql  19304  pgpfac1lem5  20146  lmhmeql  21176  rspprop  21370  islindf4  21988  1stcfb  23602  fbssfi  23994  filssufilg  24068  txflf  24163  ptcmplem3  24211  symgtgp  24263  tgpconncompeqg  24269  cnllycmp  25115  ovolgelb  25639  dyadmax  25757  lhop1  26173  radcnvlt1  26581  noextenddif  27832  conway  27972  madebdaylemlrcut  28092  oncutlt  28457  oniso  28464  bdayons  28469  bdayn0p1  28562  poimirlem4  38275  poimirlem32  38303  ismblfin  38312  igenval2  38717  glbconN  40151  nadd2rabtr  44111  isubgruhgr  48633  intubeu  49762  unilbeu  49763