Theorem ralrab 3684

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2110  ∀wral 3138  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496

This theorem is referenced by:  frminex  5534  wereu2  5551  weniso  7106  zmin  12343  prmreclem1  16251  lublecllem  17597  mhmeql  17989  ghmeql  18380  pgpfac1lem5  19200  lmhmeql  19826  islindf4  20981  1stcfb  22052  fbssfi  22444  filssufilg  22518  txflf  22613  ptcmplem3  22661  symgtgp  22713  tgpconncompeqg  22719  cnllycmp  23559  ovolgelb  24080  dyadmax  24198  lhop1  24610  radcnvlt1  25005  frpomin  33078  noextenddif  33175  conway  33264  poimirlem4  34895  poimirlem32  34923  ismblfin  34932  igenval2  35343  glbconN  36512  mgmhmeql  44069