![]() |
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 3502 | . . . 4 ⊢ (𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | imbi1i 338 | . . 3 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)) |
4 | impexp 461 | . . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) | |
5 | 3, 4 | bitri 264 | . 2 ⊢ ((𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑} → 𝜒) ↔ (𝑥 ∈ 𝐴 → (𝜓 → 𝜒))) |
6 | 5 | ralbii2 3114 | 1 ⊢ (∀𝑥 ∈ {𝑦 ∈ 𝐴 ∣ 𝜑}𝜒 ↔ ∀𝑥 ∈ 𝐴 (𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 ∈ wcel 2137 ∀wral 3048 {crab 3052 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1986 ax-6 2052 ax-7 2088 ax-9 2146 ax-10 2166 ax-11 2181 ax-12 2194 ax-13 2389 ax-ext 2738 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2045 df-clab 2745 df-cleq 2751 df-clel 2754 df-nfc 2889 df-ral 3053 df-rab 3057 df-v 3340 |
This theorem is referenced by: frminex 5244 wereu2 5261 weniso 6765 zmin 11975 prmreclem1 15820 lublecllem 17187 mhmeql 17563 ghmeql 17882 pgpfac1lem5 18676 lmhmeql 19255 islindf4 20377 1stcfb 21448 fbssfi 21840 filssufilg 21914 txflf 22009 ptcmplem3 22057 symgtgp 22104 tgpconncompeqg 22114 cnllycmp 22954 ovolgelb 23446 dyadmax 23564 lhop1 23974 radcnvlt1 24369 frpomin 32042 noextenddif 32125 conway 32214 poimirlem4 33724 poimirlem32 33752 ismblfin 33761 igenval2 34176 glbconN 35164 mgmhmeql 42311 |
Copyright terms: Public domain | W3C validator |