![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralrab | Structured version Visualization version GIF version |
Description: Universal quantification over a restricted class abstraction. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Ref | Expression |
---|---|
ralab.1 | ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralrab | ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralab.1 | . . . . 5 ⊢ (𝑦 = 𝑥 → (𝜑 ↔ 𝜓)) | |
2 | 1 | elrab 3628 | . . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | imbi1i 353 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
4 | impexp 454 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
5 | 3, 4 | bitri 278 | . 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
6 | 5 | ralbii2 3131 | 1 ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2111 ∀wral 3106 {crab 3110 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rab 3115 df-v 3443 |
This theorem is referenced by: frminex 5499 wereu2 5516 weniso 7086 zmin 12332 prmreclem1 16242 lublecllem 17590 mhmeql 17982 ghmeql 18373 pgpfac1lem5 19194 lmhmeql 19820 islindf4 20527 1stcfb 22050 fbssfi 22442 filssufilg 22516 txflf 22611 ptcmplem3 22659 symgtgp 22711 tgpconncompeqg 22717 cnllycmp 23561 ovolgelb 24084 dyadmax 24202 lhop1 24617 radcnvlt1 25013 frpomin 33191 noextenddif 33288 conway 33377 poimirlem4 35061 poimirlem32 35089 ismblfin 35098 igenval2 35504 glbconN 36673 mgmhmeql 44423 |
Copyright terms: Public domain | W3C validator |