Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbida | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Oct-2003.) |
Ref | Expression |
---|---|
ralbida.1 | ⊢ Ⅎ𝑥𝜑 |
ralbida.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbida | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbida.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbida.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 2 | pm5.74da 802 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜒))) |
4 | 1, 3 | albid 2224 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒))) |
5 | df-ral 3145 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
6 | df-ral 3145 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜒)) | |
7 | 4, 5, 6 | 3bitr4g 316 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1535 Ⅎwnf 1784 ∈ wcel 2114 ∀wral 3140 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-nf 1785 df-ral 3145 |
This theorem is referenced by: ralbid 3233 2ralbida 3234 ralbiOLD 3235 ac6num 9903 neiptopreu 21743 istrkg2ld 26248 funcnv5mpt 30415 xrralrecnnge 41669 climf2 41954 clim2f2 41958 limsupub 41992 climinfmpt 42003 limsupubuzmpt 42007 limsupre2mpt 42018 limsupre3mpt 42022 limsupreuzmpt 42027 xlimmnfmpt 42131 xlimpnfmpt 42132 smfsupmpt 43096 smfinfmpt 43100 |
Copyright terms: Public domain | W3C validator |