Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralbid | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
ralbid.1 | ⊢ Ⅎ𝑥𝜑 |
ralbid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbid | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbid.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbid.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 2 | adantr 480 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
4 | 1, 3 | ralbida 2965 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 Ⅎwnf 1699 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-ex 1696 df-nf 1701 df-ral 2901 |
This theorem is referenced by: raleqbid 3127 sbcralt 3477 sbcrext 3478 sbcrextOLD 3479 riota5f 6535 zfrep6 7027 cnfcom3clem 8485 cplem2 8636 infxpenc2lem2 8726 acnlem 8754 lble 10854 fsuppmapnn0fiubex 12654 chirred 28638 aciunf1lem 28844 indexa 32698 riotasvd 33260 cdlemk36 35219 choicefi 38387 axccdom 38411 climf 38689 climf2 38733 cncficcgt0 38774 stoweidlem16 38909 stoweidlem18 38911 stoweidlem21 38914 stoweidlem29 38922 stoweidlem31 38924 stoweidlem36 38929 stoweidlem41 38934 stoweidlem44 38937 stoweidlem45 38938 stoweidlem51 38944 stoweidlem55 38948 stoweidlem59 38952 stoweidlem60 38953 issmfgelem 39655 |
Copyright terms: Public domain | W3C validator |