Theorem ralrab 3368

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 3363	. . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	imbi1i 339	. . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
4		impexp 462	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	3, 4	bitri 264	. 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
6	5	ralbii2 2978	1 ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990  ∀wral 2912  {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202

This theorem is referenced by:  frminex  5094  wereu2  5111  weniso  6604  zmin  11784  prmreclem1  15620  lublecllem  16988  mhmeql  17364  ghmeql  17683  pgpfac1lem5  18478  lmhmeql  19055  islindf4  20177  1stcfb  21248  fbssfi  21641  filssufilg  21715  txflf  21810  ptcmplem3  21858  symgtgp  21905  tgpconncompeqg  21915  cnllycmp  22755  ovolgelb  23248  dyadmax  23366  lhop1  23777  radcnvlt1  24172  noextenddif  31821  conway  31910  poimirlem4  33413  poimirlem32  33441  ismblfin  33450  igenval2  33865  glbconN  34663  mgmhmeql  41803