Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbidva | GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1515 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | ralbida 2458 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∈ wcel 2135 ∀wral 2442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-4 1497 ax-17 1513 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 |
This theorem is referenced by: raleqbidva 2673 poinxp 4667 funimass4 5531 funimass3 5595 funconstss 5597 cocan1 5749 cocan2 5750 isocnv2 5774 isores2 5775 isoini2 5781 ofrfval 6052 ofrfval2 6060 dfsmo2 6246 smores 6251 smores2 6253 ac6sfi 6855 supisolem 6964 ordiso2 6991 ismkvnex 7110 caucvgsrlemcau 7725 suplocsrlempr 7739 axsuploc 7962 suprleubex 8840 dfinfre 8842 zextlt 9274 prime 9281 infregelbex 9527 fzshftral 10033 fimaxq 10729 clim 11208 clim2 11210 clim2c 11211 clim0c 11213 climabs0 11234 climrecvg1n 11275 mertenslem2 11463 mertensabs 11464 dfgcd2 11932 sqrt2irr 12073 pc11 12241 pcz 12242 tgss2 12626 neipsm 12701 ssidcn 12757 lmbrf 12762 cnnei 12779 cnrest2 12783 lmss 12793 lmres 12795 ismet2 12901 elmopn2 12996 metss 13041 metrest 13053 metcnp 13059 metcnp2 13060 metcn 13061 txmetcnp 13065 divcnap 13102 elcncf2 13108 mulc1cncf 13123 cncfmet 13126 cdivcncfap 13134 limcdifap 13178 limcmpted 13179 cnlimc 13188 iswomni0 13771 |
Copyright terms: Public domain | W3C validator |